diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-08-21 13:42:49 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-08-21 13:42:49 +0200 |
commit | 5fdb050e09ff5fefbe42003499de22c56b2321bb (patch) | |
tree | a927add9a3f8cea961b94a75e7b638bce19a4503 /driver/Linker.ml | |
parent | 32c34a37e913b856e0267ad8c7ca6e65b96c0b23 (diff) | |
download | compcert-5fdb050e09ff5fefbe42003499de22c56b2321bb.tar.gz compcert-5fdb050e09ff5fefbe42003499de22c56b2321bb.zip |
Fix passing of -u to linker.
Instead of just passing -u to the linker also pass the value of
the option to the linker.
Bug 24316
Diffstat (limited to 'driver/Linker.ml')
-rw-r--r-- | driver/Linker.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Linker.ml b/driver/Linker.ml index 6e6ad6b4..d6e1d384 100644 --- a/driver/Linker.ml +++ b/driver/Linker.ml @@ -86,4 +86,4 @@ let linker_actions = 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;] + Exact "-u", String (fun s -> push_linker_arg "-u"; push_linker_arg s);] |