From 22eb2d34f0a9249720a30c6cb2973993e97834ea Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 18 May 2015 15:39:55 +0200
Subject: Fix usage about -color.

---
 toplevel/usage.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 50fb019f47..36ecc9fa5f 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -58,7 +58,7 @@ let print_usage_channel co command =
 \n\
 \n  -quiet                 unset display of extra information (implies -w none)\
 \n  -w (all|none)          configure display of warnings\
-\n  -color (on|off|auto)   configure color output (only active through coqtop)\
+\n  -color (on|off|auto)   configure color output\
 \n\
 \n  -q                     skip loading of rcfile\
 \n  -init-file f           set the rcfile to f\
-- 
cgit v1.2.3