From 076e8fb1e20b5bc77e3a5d7011cd7b229fcc017d Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 22 Jun 2016 10:35:19 +0200
Subject: Driveraux.mli: fix documentation comment

---
 driver/Driveraux.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'driver/Driveraux.mli')

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 *)
-- 
cgit