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/Linker.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/Linker.ml')
| -rw-r--r-- | driver/Linker.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/driver/Linker.ml b/driver/Linker.ml index 5e14cfd4..54566efb 100644 --- a/driver/Linker.ml +++ b/driver/Linker.ml @@ -48,7 +48,7 @@ let linker_help = -l<lib> Link library <lib> -L<dir> Add <dir> to search path for libraries |} ^ - (if gnu_system then gnu_linker_help else "") ^ + (if Configuration.gnu_toolchain then gnu_linker_help else "") ^ {| -s Remove all symbol table and relocation information from the executable -static Prevent linking with the shared libraries @@ -63,14 +63,14 @@ let linker_help = let linker_actions = [ Prefix "-l", Self push_linker_arg; Prefix "-L", Self push_linker_arg; ] @ - (if gnu_system then + (if Configuration.gnu_toolchain then [ Exact "-nostartfiles", Self push_linker_arg; Exact "-nodefaultlibs", Self push_linker_arg; Exact "-nostdlib", Self push_linker_arg;] else []) @ [ Exact "-s", Self push_linker_arg; Exact "-static", Self push_linker_arg; - Exact "-T", String (fun s -> if gnu_system then begin + Exact "-T", String (fun s -> if Configuration.gnu_toolchain then begin push_linker_arg ("-T"); push_linker_arg(s) end else |