diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-16 14:05:11 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-16 14:23:56 +0200 |
| commit | 01847d2c992b05af5ed477ec7a208064526b0c5f (patch) | |
| tree | 8b91c2fa969205e0bb151f49c7432f78e58ddefb /toplevel | |
| parent | 7ded7df853fd0485822f2a9c79207352af5dca38 (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.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | toplevel/usage.ml | 4 | ||||
| -rw-r--r-- | toplevel/usage.mli | 1 |
3 files changed, 6 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a820008d2..46fb55b5f 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 ffbbe7ed4..8f77aea44 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 3ce9e93ee..dccb40e71 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 |