diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-05-13 09:29:09 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-05-13 09:29:09 +0200 |
commit | 19f2a76f9b5ea3503c2cb8d3153f212e77eda92d (patch) | |
tree | 86dd27dbd17baae5485fb5471d2f4327c5a87519 | |
parent | 0d48fd07e551d3cedd616126400b00464a137835 (diff) | |
download | compcert-19f2a76f9b5ea3503c2cb8d3153f212e77eda92d.tar.gz compcert-19f2a76f9b5ea3503c2cb8d3153f212e77eda92d.zip |
Added option to pass linker options to gcc.
Some gcc options have influence on the linking (especially -march,
etc.). The new -WUl options allows it to pass the options to the
gcc called for linking instead of passing them to the linker
directly.
Bug 18949.
-rw-r--r-- | driver/Driver.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 17d7b997..567ff018 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -551,6 +551,7 @@ Linking options: -static Prevent linking with the shared libraries -T <file> Use <file> as linker command file -Wl,<opt> Pass option <opt> to the linker + -WUl,<opt> (GCC only) Pass option <opt> to the gcc used for linking -Xlinker <opt> Pass <opt> as an option to the linker -u <symb> Pretend the symbol <symb> is undefined to force linking of library modules to define it. @@ -738,6 +739,7 @@ let cmdline_actions = else push_linker_arg s); Prefix "-Wl,", Self push_linker_arg; + Prefix "-WUl,", Self (fun s -> List.iter push_linker_arg (explode_comma_option s)); Exact "-u", Self push_linker_arg; (* Tracing options *) Exact "-dprepro", Set option_dprepro; |