diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-15 19:42:34 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-15 19:42:34 +0100 |
commit | d549e018fd5d4a9429025399885ed04d40b5de97 (patch) | |
tree | 056e21593017a5dd30293150fbdd866381da38ab /toplevel/usage.ml | |
parent | 4f8ac37d1e69c1e8889bb9bebd20ceeadc9c72cc (diff) |
Adding a command line option to print out accepted color tags.
Diffstat (limited to 'toplevel/usage.ml')
-rw-r--r-- | toplevel/usage.ml | 1 |
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\ |