From efa462bd1655c6b2c8f064e214762650092257e8 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 12 Jul 2016 13:18:42 +0200 Subject: 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 --- driver/Driveraux.mli | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'driver/Driveraux.mli') 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. *) -- cgit