diff options
Diffstat (limited to 'driver/Driveraux.mli')
| -rw-r--r-- | driver/Driveraux.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli index e6bac6e3..274ecedd 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -36,9 +36,6 @@ val ensure_inputfile_exists: string -> unit val print_error:out_channel -> Errors.errcode list -> unit (** Printing of error messages *) -val gnu_system: bool - (** Are the target tools gnu tools? *) - val explode_comma_option: string -> string list (** Split option at commas *) |