aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
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 /tools
parent11ec801fa17434b0a3aad2c88a4422a22f1c4c44 (diff)
Document --print-version in Usage
Diffstat (limited to 'tools')
-rw-r--r--tools/coqc.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml
index e9f79212b..9857d4318 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -85,6 +85,9 @@ let parse_args () =
Envars.set_coqlib ~fail:(fun x -> x);
Envars.print_config stdout;
exit 0
+
+ |"--print-version" :: _ ->
+ Usage.machine_readable_version 0
(* Options for coqtop : a) options with 0 argument *)