aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-01-05 16:57:58 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-05-23 10:48:28 +0200
commit577f6d0e5c4eecca3a3cd46dfc37084123f4adf6 (patch)
tree90fe844bd7322faf2bba1e474abd911b27952075 /toplevel
parent11ec801fa17434b0a3aad2c88a4422a22f1c4c44 (diff)
Document --print-version in Usage
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/usage.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 67701d73e..c43f0ff05 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -56,7 +56,8 @@ let print_usage_channel co command =
\n\
\n -where print Coq's standard library location and exit\
\n -config, --config print Coq's configuration information and exit\
-\n -v print Coq version and exit\
+\n -v, --version print Coq version and exit\
+\n --print-version print Coq version in easy to parse format and exit\
\n -list-tags print highlight color tags known by Coq and exit\
\n\
\n -quiet unset display of extra information (implies -w \"-all\")\