diff options
Diffstat (limited to 'driver/main_args.mli')
| -rw-r--r-- | driver/main_args.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/main_args.mli b/driver/main_args.mli index ff284a985a..2249ab20c7 100644 --- a/driver/main_args.mli +++ b/driver/main_args.mli @@ -83,6 +83,7 @@ module type Bytetop_options = sig val _nostdlib : unit -> unit val _principal : unit -> unit val _rectypes : unit -> unit + val _stdin : unit -> unit val _strict_sequence : unit -> unit val _unsafe : unit -> unit val _version : unit -> unit @@ -183,6 +184,7 @@ module type Opttop_options = sig val _principal : unit -> unit val _rectypes : unit -> unit val _S : unit -> unit + val _stdin : unit -> unit val _strict_sequence : unit -> unit val _unsafe : unit -> unit val _version : unit -> unit |