diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-19 09:44:26 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-19 09:44:26 +0200 |
| commit | 2129fe8f2e19c4dd91955e5300e76d924e0a3e6d (patch) | |
| tree | 142db2c4fd4931dc7b2d6cfb1bf77e8f4e5ec584 /driver/Driveraux.mli | |
| parent | efa462bd1655c6b2c8f064e214762650092257e8 (diff) | |
| download | compcert-kvx-2129fe8f2e19c4dd91955e5300e76d924e0a3e6d.tar.gz compcert-kvx-2129fe8f2e19c4dd91955e5300e76d924e0a3e6d.zip | |
Merged responfile function into command.
Command now decides whether to use a responsefile or call the
external command directly.
Bug 18004
Diffstat (limited to 'driver/Driveraux.mli')
| -rw-r--r-- | driver/Driveraux.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli index 54df4336..e6bac6e3 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -12,12 +12,6 @@ (* *********************************************************************) -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. *) |