diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-19 09:44:26 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-19 09:44:26 +0200 |
commit | 2129fe8f2e19c4dd91955e5300e76d924e0a3e6d (patch) | |
tree | 142db2c4fd4931dc7b2d6cfb1bf77e8f4e5ec584 /driver/Driveraux.ml | |
parent | efa462bd1655c6b2c8f064e214762650092257e8 (diff) | |
download | compcert-2129fe8f2e19c4dd91955e5300e76d924e0a3e6d.tar.gz compcert-2129fe8f2e19c4dd91955e5300e76d924e0a3e6d.zip |
Merged responfile function into command.
Command now decides whether to use a responsefile or call the
external command directly.
Bug 18004
Diffstat (limited to 'driver/Driveraux.ml')
-rw-r--r-- | driver/Driveraux.ml | 49 |
1 files changed, 27 insertions, 22 deletions
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 8ebf261d..2c03c65c 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -17,31 +17,17 @@ open Clflags (* Is this a gnu based tool chain *) let gnu_system = Configuration.system <> "diab" +(* Sage removale of files *) +let safe_remove file = + try Sys.remove file with Sys_error _ -> () + (* 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 = +let command stdout args = if !option_v then begin eprintf "+ %s" (String.concat " " args); begin match stdout with @@ -72,12 +58,31 @@ let command ?stdout args = argv.(0) fn (Unix.error_message err) param; -1 +let quote arg = + let whitespace = Str.regexp "[ \t\r\n]" in + if Str.string_match whitespace arg 0 then + Filename.quote arg (* We need to quote arguments containing whitespaces *) + else + arg + +let command ?stdout args = + if Sys.win32 && List.fold_left (fun len arg -> len + String.length arg + 1) 0 args > 7000 then + let file,oc = Filename.open_temp_file "compcert" "" in + let cmd,args = match args with + | cmd::args -> cmd,args + | [] -> assert false (* Should never happen *) in + List.iter (fun a -> Printf.fprintf oc "%s " (quote a)) args; + close_out oc; + let arg = if gnu_system then "@"^file else "-@"^file in + let ret = command stdout [cmd;arg] in + safe_remove file; + ret + else + command stdout args + let command_error n exc = eprintf "Error: %s command failed with exit code %d (use -v to see invocation)\n" n exc -let safe_remove file = - try Sys.remove file with Sys_error _ -> () - (* Determine names for output files. We use -o option if specified and if this is the final destination file (not a dump file). |