diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-22 13:34:56 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-22 13:34:56 +0200 |
commit | 0200f6b77550e95c0ec309d1a44f5253fc790e4f (patch) | |
tree | 7c27cf00a408165fc9c54fba1879f3f76ae2d12c /driver | |
parent | 2084c5b91929b9290b7e02979ee038bb98d1053e (diff) | |
download | compcert-0200f6b77550e95c0ec309d1a44f5253fc790e4f.tar.gz compcert-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')
-rw-r--r-- | driver/Driveraux.ml | 16 |
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 |