aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/usage.ml2
1 files changed, 1 insertions, 1 deletions
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\