diff options
Diffstat (limited to 'driver/main.ml')
| -rw-r--r-- | driver/main.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/main.ml b/driver/main.ml index 8e1f58fbe7..b1ac5b0390 100644 --- a/driver/main.ml +++ b/driver/main.ml @@ -80,6 +80,7 @@ module Options = Main_args.Make_options (struct let _custom = set custom_runtime let _dllib s = dllibs := Misc.rev_split_words s @ !dllibs let _dllpath s = dllpaths := !dllpaths @ [s] + let _dtypes = set save_types let _g = set debug let _i = set print_types let _I s = include_dirs := s :: !include_dirs |