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/Configuration.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/Configuration.mli')
| -rw-r--r-- | driver/Configuration.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/driver/Configuration.mli b/driver/Configuration.mli index 197e8ad2..f0bb8f83 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -74,3 +74,6 @@ type response_file_style = val response_file_style: response_file_style (** Style of supported responsefiles *) + +val gnu_toolchain: bool + (** Does the targeted system use the gnu toolchain *) |