aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--driver/Driver.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index d628e283..7832e6d2 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -568,7 +568,7 @@ let cmdline_actions =
Prefix "-l", Self push_linker_arg;
Prefix "-L", Self push_linker_arg;
Exact "-T", String (fun s -> if Configuration.system = "diab" then
- push_linker_arg ("-Wm "^s)
+ push_linker_arg ("-Wm"^s)
else
push_linker_arg ("-T "^s));
Prefix "-Wl,", Self push_linker_arg;