aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqargs.mli
diff options
context:
space:
mode:
authorHugo Herbelin2019-05-08 22:42:48 +0200
committerEmilio Jesus Gallego Arias2019-07-08 02:31:27 +0200
commitfe487e8eaae3186803ec657c517d0ebebab3bafd (patch)
tree238ae5e8285c9c20bb75f860dab460e4b647b2a6 /toplevel/coqargs.mli
parentcc9a10182255527959fc10bd86f18a7b40ef5a2a (diff)
An even more uniform treatment of the -help option across executables.
Incidentally fix some missing newline in coqc help, and give proper help for coqidetop and the "coq*worker"s.
Diffstat (limited to 'toplevel/coqargs.mli')
-rw-r--r--toplevel/coqargs.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index d1873bcb58..46220cd1d8 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -56,7 +56,7 @@ type coqargs_pre = {
type coqargs_query =
| PrintTags | PrintWhere | PrintConfig
| PrintVersion | PrintMachineReadableVersion
- | PrintHelp of (unit -> unit)
+ | PrintHelp of (out_channel -> unit)
type coqargs_main =
| Queries of coqargs_query list
@@ -77,7 +77,7 @@ type t = {
(* Default options *)
val default : t
-val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list
+val parse_args : help:(out_channel -> unit) -> init:t -> string list -> t * string list
val error_wrong_arg : string -> unit
val require_libs : t -> (string * string option * bool option) list