diff options
Diffstat (limited to 'driver/optmain.ml')
| -rw-r--r-- | driver/optmain.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/optmain.ml b/driver/optmain.ml index b84cac8ec4..8c80d47bea 100644 --- a/driver/optmain.ml +++ b/driver/optmain.ml @@ -110,6 +110,7 @@ module Options = Main_args.Make_optcomp_options (struct let _a = set make_archive let _absname = set Location.absname let _annot = set annotations + let _binannot = set binary_annotations let _c = set compile_only let _cc s = c_compiler := Some s let _cclib s = ccobjs := Misc.rev_split_words s @ !ccobjs |