From 5c0c02e51a76183eb43b5ed80d925f3c2ce88dfb Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 13 Feb 2017 15:39:07 +0100
Subject: 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.
---
 driver/Driveraux.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'driver/Driveraux.mli')

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 *)
 
-- 
cgit