summaryrefslogtreecommitdiff
path: root/toplevel/usage.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/usage.mli')
-rw-r--r--toplevel/usage.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 3ce9e93e..dccb40e7 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