diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 12:21:47 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 12:21:47 +0200 |
commit | a6bde8ba057ff057e311781fd91b4a9ab441731c (patch) | |
tree | e2d5f2f270364eefc5012870d2412dfbf7178043 | |
parent | 1ad10395dc17a4257d26e8a854cb98e7107ceff5 (diff) | |
download | compcert-a6bde8ba057ff057e311781fd91b4a9ab441731c.tar.gz compcert-a6bde8ba057ff057e311781fd91b4a9ab441731c.zip |
Really added the function. Bug 18308
-rw-r--r-- | lib/Responsefile.ml | 16 | ||||
-rw-r--r-- | lib/Responsefile.mli | 6 |
2 files changed, 19 insertions, 3 deletions
diff --git a/lib/Responsefile.ml b/lib/Responsefile.ml index c10fe302..6dd1bc93 100644 --- a/lib/Responsefile.ml +++ b/lib/Responsefile.ml @@ -131,3 +131,19 @@ let expand_responsefiles args = acc := file::!acc done; Array.of_list !acc + +let write_responsefile oc args start = + 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 + let first = ref true in + let sep oc = if !first then + first := false + else + output_string oc " " in + for i = start to (Array.length args -1) do + Printf.fprintf oc "%t%s" sep (quote args.(i)) + done diff --git a/lib/Responsefile.mli b/lib/Responsefile.mli index 2522b7c5..95c74bda 100644 --- a/lib/Responsefile.mli +++ b/lib/Responsefile.mli @@ -19,6 +19,6 @@ val expand_responsefiles: string array -> string array (** Expand responsefile arguments contained in the array and return the full set of arguments. *) -val write_responsefile: out_channel -> string array -> unit - (** Write the arguments on the out_channel. All arguments that contain - whitespaces are quoted. *) +val write_responsefile: out_channel -> string array -> int -> unit + (** Write the arguments starting at the given index as repsonsefile on the given + out_channel. All arguments that contain whitespaces are quoted. *) |