diff options
Diffstat (limited to 'driver/main_args.mli')
| -rw-r--r-- | driver/main_args.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/driver/main_args.mli b/driver/main_args.mli index 27fb475ae0..6f77a29708 100644 --- a/driver/main_args.mli +++ b/driver/main_args.mli @@ -208,8 +208,6 @@ module type Optcommon_options = sig val _dcombine : unit -> unit val _dcse : unit -> unit val _dlive : unit -> unit - val _davail : unit -> unit - val _drunavail : unit -> unit val _dspill : unit -> unit val _dsplit : unit -> unit val _dinterf : unit -> unit |