aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-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