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 /driver/Driveraux.mli | |
| parent | a6bde8ba057ff057e311781fd91b4a9ab441731c (diff) | |
| download | compcert-kvx-efa462bd1655c6b2c8f064e214762650092257e8.tar.gz compcert-kvx-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 'driver/Driveraux.mli')
| -rw-r--r-- | driver/Driveraux.mli | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli index 60efcc80..54df4336 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -12,7 +12,13 @@ (* *********************************************************************) -val command: ?stdout:string -> string list -> int +val responsefile: string list -> (string -> string list) -> string list + (** [responsefiles args resp_arg] Test whether [args] should be passed + via responsefile and writes them into a file. [resp_arg] generates + the new argument constructed from the responsefile. If no + responsefile is written the arguments are returned unchanged. *) + +val command: ?stdout:string -> string list -> int (** Execute the command with the given arguments and an optional file for the stdout. Returns the exit code. *) |