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

1 files changed, 21 insertions, 2 deletions

diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml
index 3fe22fac..8ebf261d 100644
--- a/driver/Driveraux.ml
+++ b/driver/Driveraux.ml
@@ -14,12 +14,33 @@
 open Printf
 open Clflags
 
+(* Is this a gnu based tool chain *)
+let gnu_system = Configuration.system <> "diab"
+
 (* Invocation of external tools *)
 
 let rec waitpid_no_intr pid =
   try Unix.waitpid [] pid
   with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_no_intr pid
 
+let responsefile args resp_arg =
+  try
+    if Sys.win32 && (String.length (String.concat "" args) > 7000) then
+      let file,oc = Filename.open_temp_file "compcert" "" in
+      let whitespace = Str.regexp "[ \t\r\n]" in
+      let quote arg =
+        if Str.string_match whitespace arg 0 then
+          Filename.quote arg (* We need to quote arguments containing whitespaces *)
+        else
+          arg in
+      List.iter (fun a -> Printf.fprintf oc "%s " (quote a)) args;
+      close_out oc;
+      resp_arg file
+    else
+      args
+  with Sys_error _ ->
+    args
+
 let command ?stdout args =
   if !option_v then begin
     eprintf "+ %s" (String.concat " " args);
@@ -94,8 +115,6 @@ let print_error oc msg =
     List.iter print_one_error msg;
     output_char oc '\n'
 
-let gnu_system = Configuration.system <> "diab"
-
 (* Command-line parsing *)
 let explode_comma_option s =
   match Str.split (Str.regexp ",") s with