aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEnrico Tassi2016-06-16 14:05:11 +0200
committerEnrico Tassi2016-06-16 14:23:56 +0200
commit01847d2c992b05af5ed477ec7a208064526b0c5f (patch)
tree8b91c2fa969205e0bb151f49c7432f78e58ddefb
parent7ded7df853fd0485822f2a9c79207352af5dca38 (diff)
--print-version produces machine readable version info
What one needs to know in 3rd party makefiles, like plugins ones, is the Coq version and the OCaml version number. This option prints the 2 values on a single line separated by spaces. The already existing --version outputs the same piece of info but in a format meant for user consumption, and hence harder to parse.
-rw-r--r--CHANGES2
-rw-r--r--toplevel/coqtop.ml1
-rw-r--r--toplevel/usage.ml4
-rw-r--r--toplevel/usage.mli1
4 files changed, 8 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index ae9b979292..15110e701d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -34,6 +34,8 @@ Notations
Tools
- coqc accepts a -o option to specify the output file name
+- coqtop accepts --print-version to print Coq and OCaml versions in
+ easy to parse format
Changes from V8.5pl1 to V8.5pl2
===============================
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a820008d2e..46fb55b5f7 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -575,6 +575,7 @@ let parse_args arglist =
|"-type-in-type" -> set_type_in_type ()
|"-unicode" -> add_require "Utf8_core"
|"-v"|"--version" -> Usage.version (exitcode ())
+ |"--print-version" -> Usage.machine_readable_version (exitcode ())
|"-verbose-compat-notations" -> verb_compat_ntn := true
|"-where" -> print_where := true
|"-xml" -> Flags.xml_export := true
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index ffbbe7ed4a..8f77aea440 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -11,6 +11,10 @@ let version ret =
Coq_config.version Coq_config.date;
Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version;
exit ret
+let machine_readable_version ret =
+ Printf.printf "%s %s\n"
+ Coq_config.version Coq_config.caml_version;
+ exit ret
(* print the usage of coqtop (or coqc) on channel co *)
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 3ce9e93ee5..dccb40e713 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -9,6 +9,7 @@
(** {6 Prints the version number on the standard output and exits (with 0). } *)
val version : int -> 'a
+val machine_readable_version : int -> 'a
(** {6 Prints the usage on the error output, preceeded by a user-provided message. } *)
val print_usage : string -> unit