From 0200f6b77550e95c0ec309d1a44f5253fc790e4f Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 22 Aug 2016 13:34:56 +0200
Subject: 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.
---
 driver/Driveraux.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'driver/Driveraux.ml')

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
-- 
cgit