aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Responsefile.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-07-11 12:21:47 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-07-11 12:21:47 +0200
commita6bde8ba057ff057e311781fd91b4a9ab441731c (patch)
treee2d5f2f270364eefc5012870d2412dfbf7178043 /lib/Responsefile.ml
parent1ad10395dc17a4257d26e8a854cb98e7107ceff5 (diff)
downloadcompcert-a6bde8ba057ff057e311781fd91b4a9ab441731c.tar.gz
compcert-a6bde8ba057ff057e311781fd91b4a9ab441731c.zip
Really added the function. Bug 18308
Diffstat (limited to 'lib/Responsefile.ml')
-rw-r--r--lib/Responsefile.ml16
1 files changed, 16 insertions, 0 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