aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Linker.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-07-12 13:18:42 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-07-12 13:18:42 +0200
commitefa462bd1655c6b2c8f064e214762650092257e8 (patch)
treefbabaeb77489660a60666accdef6bfbb89495478 /driver/Linker.ml
parenta6bde8ba057ff057e311781fd91b4a9ab441731c (diff)
downloadcompcert-efa462bd1655c6b2c8f064e214762650092257e8.tar.gz
compcert-efa462bd1655c6b2c8f064e214762650092257e8.zip
Added heuristic for passing arg via responsefiles.
Since gnu make and other tools under windows seem to have a limit of around 8000 bytes per command line the arguments should be passed via responsefiles instead. Bug 18308
Diffstat (limited to 'driver/Linker.ml')
-rw-r--r--driver/Linker.ml13
1 files changed, 9 insertions, 4 deletions
diff --git a/driver/Linker.ml b/driver/Linker.ml
index 2f767023..14c9bcb3 100644
--- a/driver/Linker.ml
+++ b/driver/Linker.ml
@@ -19,14 +19,19 @@ open Driveraux
(* Linking *)
let linker exe_name files =
- let cmd = List.concat [
- Configuration.linker;
+ let cmd,opts = match Configuration.linker with
+ | name::opts -> name,opts
+ | [] -> assert false (* Should be catched in Configuration *) in
+ let opts = List.concat [
+ opts;
["-o"; exe_name];
files;
(if Configuration.has_runtime_lib
- then ["-L" ^ !stdlib_path; "-lcompcert"]
- else [])
+ then ["-L" ^ !stdlib_path; "-lcompcert"]
+ else [])
] in
+ let opts = responsefile opts (fun a -> if gnu_system then ["@"^a] else ["-@"^a]) in
+ let cmd = cmd::opts in
let exc = command cmd in
if exc <> 0 then begin
command_error "linker" exc;