diff options
Diffstat (limited to 'driver/Driveraux.mli')
| -rw-r--r-- | driver/Driveraux.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli index 60efcc80..e6bac6e3 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -12,7 +12,7 @@ (* *********************************************************************) -val command: ?stdout:string -> string list -> int +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. *) |