diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-12 13:18:42 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-12 13:18:42 +0200 |
| commit | efa462bd1655c6b2c8f064e214762650092257e8 (patch) | |
| tree | fbabaeb77489660a60666accdef6bfbb89495478 /lib | |
| parent | a6bde8ba057ff057e311781fd91b4a9ab441731c (diff) | |
| download | compcert-efa462bd1655c6b2c8f064e214762650092257e8.tar.gz compcert-efa462bd1655c6b2c8f064e214762650092257e8.zip | |
Added heuristic for passing arg via responsefiles.
Since gnu make and other tools under windows seem to have a limit
of around 8000 bytes per command line the arguments should be
passed via responsefiles instead.
Bug 18308
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Responsefile.ml | 16 | ||||
| -rw-r--r-- | lib/Responsefile.mli | 4 |
2 files changed, 0 insertions, 20 deletions
diff --git a/lib/Responsefile.ml b/lib/Responsefile.ml index 6dd1bc93..c10fe302 100644 --- a/lib/Responsefile.ml +++ b/lib/Responsefile.ml @@ -131,19 +131,3 @@ 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 95c74bda..b55dac16 100644 --- a/lib/Responsefile.mli +++ b/lib/Responsefile.mli @@ -18,7 +18,3 @@ 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 -> int -> unit - (** Write the arguments starting at the given index as repsonsefile on the given - out_channel. All arguments that contain whitespaces are quoted. *) |