diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-13 15:39:07 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-13 15:39:07 +0100 |
| commit | 5c0c02e51a76183eb43b5ed80d925f3c2ce88dfb (patch) | |
| tree | 13266f8767648ee5433f30b16ec503144c67d003 /driver/Driveraux.mli | |
| parent | 236d8a48288ea5845466408cf9d0be2ccd68f9a8 (diff) | |
| download | compcert-kvx-5c0c02e51a76183eb43b5ed80d925f3c2ce88dfb.tar.gz compcert-kvx-5c0c02e51a76183eb43b5ed80d925f3c2ce88dfb.zip | |
Introduced configuration variable for gnu systems.
The variable gnu_toolchain is true if a gnu toolchain is used and
false in all other cases. The variable avoids the explicit test
whether the system string is diab and should be easier to change.
Bug 20521.
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 *) |