diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-06 12:37:31 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-06 12:37:31 +0200 |
| commit | e8127be72ffc16f91de51c0b8dca3df0d3bd4745 (patch) | |
| tree | fcb44286732a66e9457fb671185f7f888fe7aaa7 /driver | |
| parent | 55eb2d92376f592258855cfa5c0cfbbf39e8e833 (diff) | |
| download | compcert-e8127be72ffc16f91de51c0b8dca3df0d3bd4745.tar.gz compcert-e8127be72ffc16f91de51c0b8dca3df0d3bd4745.zip | |
Push the linker args separate.
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 9b1a6e70..c7d9984e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -572,8 +572,10 @@ let cmdline_actions = Prefix "-L", Self push_linker_arg; Exact "-T", String (fun s -> if Configuration.system = "diab" then push_linker_arg ("-Wm"^s) - else - push_linker_arg ("-T "^s)); + else begin + push_linker_arg ("-T"); + push_linker_arg(s) + end); Prefix "-Wl,", Self push_linker_arg; (* Tracing options *) Exact "-dparse", Set option_dparse; |