aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driveraux.mli
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2016-06-22 10:35:19 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2016-06-22 10:35:19 +0200
commit076e8fb1e20b5bc77e3a5d7011cd7b229fcc017d (patch)
tree7f3fd52e7d702388936cbc52c54438f40c1d46c2 /driver/Driveraux.mli
parent7237ccb621d58b2c86ef250f1c3e3ffd29260955 (diff)
downloadcompcert-kvx-076e8fb1e20b5bc77e3a5d7011cd7b229fcc017d.tar.gz
compcert-kvx-076e8fb1e20b5bc77e3a5d7011cd7b229fcc017d.zip
Driveraux.mli: fix documentation comment
Diffstat (limited to 'driver/Driveraux.mli')
-rw-r--r--driver/Driveraux.mli2
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 *)