diff options
Diffstat (limited to 'otherlibs/labltk/browser/editor.ml')
| -rw-r--r-- | otherlibs/labltk/browser/editor.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/otherlibs/labltk/browser/editor.ml b/otherlibs/labltk/browser/editor.ml index d0ed98cbc..fc8edbca6 100644 --- a/otherlibs/labltk/browser/editor.ml +++ b/otherlibs/labltk/browser/editor.ml @@ -39,6 +39,7 @@ let compiler_preferences () = [ "No pervasives", Clflags.nopervasives, false; "No warnings", Typecheck.nowarnings, false; "Labels commute", Clflags.classic, true; + "Recursive types", Clflags.recursive_types, false; "Lex on load", lex_on_load, false; "Type on load", type_on_load, false ]) in |