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.ml | |
| 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.ml')
| -rw-r--r-- | driver/Driveraux.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index d25301d2..2c478fb1 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -14,9 +14,6 @@ open Printf open Clflags -(* Is this a gnu based tool chain *) -let gnu_system = Configuration.system <> "diab" - (* Safe removal of files *) let safe_remove file = try Sys.remove file with Sys_error _ -> () |