aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Linker.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-08-16 10:35:17 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-08-16 10:35:17 +0200
commit5309f16159e4decd81330622dcdd6eb4b25819a1 (patch)
treeb40df6edcd7826e7d83885253508ccf49377479d /driver/Linker.ml
parenteb2844b87fa0e176bd65466d7ab7d16666344406 (diff)
downloadcompcert-5309f16159e4decd81330622dcdd6eb4b25819a1.tar.gz
compcert-5309f16159e4decd81330622dcdd6eb4b25819a1.zip
Moved quoting functions in Responsefile
Also corrected some typos and corrected exception handling for expandargv. Bug 18308
Diffstat (limited to 'driver/Linker.ml')
-rw-r--r--driver/Linker.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/driver/Linker.ml b/driver/Linker.ml
index 305c5603..2f767023 100644
--- a/driver/Linker.ml
+++ b/driver/Linker.ml
@@ -24,8 +24,8 @@ let linker exe_name files =
["-o"; exe_name];
files;
(if Configuration.has_runtime_lib
- then ["-L" ^ !stdlib_path; "-lcompcert"]
- else [])
+ then ["-L" ^ !stdlib_path; "-lcompcert"]
+ else [])
] in
let exc = command cmd in
if exc <> 0 then begin