diff options
Diffstat (limited to 'driver/main_args.mli')
| -rw-r--r-- | driver/main_args.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/main_args.mli b/driver/main_args.mli index f3b6cd59fb..1dff86e795 100644 --- a/driver/main_args.mli +++ b/driver/main_args.mli @@ -18,6 +18,7 @@ module type Common_options = sig val _absname : unit -> unit + val _alert : string -> unit val _I : string -> unit val _labels : unit -> unit val _alias_deps : unit -> unit |