aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/usage.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-11-15 19:42:34 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-11-15 19:42:34 +0100
commitd549e018fd5d4a9429025399885ed04d40b5de97 (patch)
tree056e21593017a5dd30293150fbdd866381da38ab /toplevel/usage.ml
parent4f8ac37d1e69c1e8889bb9bebd20ceeadc9c72cc (diff)
Adding a command line option to print out accepted color tags.
Diffstat (limited to 'toplevel/usage.ml')
-rw-r--r--toplevel/usage.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e098f70a8..1efccefba 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -51,6 +51,7 @@ let print_usage_channel co command =
\n -where print Coq's standard library location and exit\
\n -config print Coq's configuration information and exit\
\n -v print Coq version and exit\
+\n -list-tags print highlight color tags known by Coq and exit\
\n\
\n -q skip loading of rcfile\
\n -init-file f set the rcfile to f\