aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driveraux.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-08-22 13:34:56 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-08-22 13:34:56 +0200
commit0200f6b77550e95c0ec309d1a44f5253fc790e4f (patch)
tree7c27cf00a408165fc9c54fba1879f3f76ae2d12c /driver/Driveraux.ml
parent2084c5b91929b9290b7e02979ee038bb98d1053e (diff)
downloadcompcert-kvx-0200f6b77550e95c0ec309d1a44f5253fc790e4f.tar.gz
compcert-kvx-0200f6b77550e95c0ec309d1a44f5253fc790e4f.zip
Print whole command line.
When response files are used CompCert should still print all command line arguments since the response file is deleted after usage. Bug 19297.
Diffstat (limited to 'driver/Driveraux.ml')
-rw-r--r--driver/Driveraux.ml16
1 files changed, 8 insertions, 8 deletions
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml
index 33cd9215..d25301d2 100644
--- a/driver/Driveraux.ml
+++ b/driver/Driveraux.ml
@@ -28,14 +28,6 @@ let rec waitpid_no_intr pid =
with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_no_intr pid
let command stdout args =
- if !option_v then begin
- eprintf "+ %s" (String.concat " " args);
- begin match stdout with
- | None -> ()
- | Some f -> eprintf " > %s" f
- end;
- prerr_endline ""
- end;
let argv = Array.of_list args in
assert (Array.length argv > 0);
try
@@ -59,6 +51,14 @@ let command stdout args =
-1
let command ?stdout args =
+ if !option_v then begin
+ eprintf "+ %s" (String.concat " " args);
+ begin match stdout with
+ | None -> ()
+ | Some f -> eprintf " > %s" f
+ end;
+ prerr_endline ""
+ end;
let resp = Sys.win32 && Configuration.response_file_style <> Configuration.Unsupported in
if resp && List.fold_left (fun len arg -> len + String.length arg + 1) 0 args > 7000 then
let quote,prefix = match Configuration.response_file_style with