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 539b1797..1cb219a1 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -40,4 +40,4 @@ val gnu_option: string -> bool (** Set the options for gnu systems *) val explode_comma_option: string -> string list - (** Split options by whitespace *) + (** Split option at commas *) |