diff options
Diffstat (limited to 'toplevel/topmain.ml')
| -rw-r--r-- | toplevel/topmain.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/topmain.ml b/toplevel/topmain.ml index b63eefcb43..3a4adcbd88 100644 --- a/toplevel/topmain.ml +++ b/toplevel/topmain.ml @@ -54,6 +54,7 @@ module Options = Main_args.Make_bytetop_options (struct let set r () = r := true let clear r () = r := false + let _help_warnings = Warnings.help_warnings let _I dir = let dir = Misc.expand_directory Config.standard_library dir in include_dirs := dir :: !include_dirs |