From efa462bd1655c6b2c8f064e214762650092257e8 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 12 Jul 2016 13:18:42 +0200 Subject: 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 --- driver/Frontend.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'driver/Frontend.ml') diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 043d4e5a..41b09b58 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -24,8 +24,11 @@ open Printf let preprocess ifile ofile = let output = if ofile = "-" then None else Some ofile in - let cmd = List.concat [ - Configuration.prepro; + let cmd,opts = match Configuration.prepro with + | name::opts -> name,opts + | [] -> assert false (* Should be catched in Configuration *) in + let opts = List.concat [ + opts; ["-D__COMPCERT__"]; (if !Clflags.use_standard_headers then ["-I" ^ Filename.concat !Clflags.stdlib_path "include" ] @@ -33,6 +36,8 @@ let preprocess ifile ofile = List.rev !prepro_options; [ifile] ] in + let opts = responsefile opts (fun a -> if gnu_system then ["@"^a] else ["@"^a]) in + let cmd = cmd::opts in let exc = command ?stdout:output cmd in if exc <> 0 then begin if ofile <> "-" then safe_remove ofile; -- cgit