diff options
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/main_args.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/main_args.ml b/driver/main_args.ml index f0b06b9636..667158503b 100644 --- a/driver/main_args.ml +++ b/driver/main_args.ml @@ -1185,6 +1185,7 @@ struct mk_cc F._cc; mk_cclib F._cclib; mk_ccopt F._ccopt; + mk_cmi_file F._cmi_file; mk_clambda_checks F._clambda_checks; mk_classic_inlining F._classic_inlining; mk_color F._color; |