diff options
| author | Hugo Herbelin | 2019-05-10 09:36:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 02:31:27 +0200 |
| commit | f2779d48d3b7735687444e22b16cdb7cb8f7ce60 (patch) | |
| tree | 5c17149292f54e3bfe3b4d3977825a10c3de8a92 /ide | |
| parent | fe487e8eaae3186803ec657c517d0ebebab3bafd (diff) | |
Usage: bypassing a useless detour via a reference.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/idetop.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml index eb76951b44..02682e2ee9 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -552,11 +552,15 @@ let rec parse = function x :: parse rest | [] -> [] -let () = Usage.add_to_usage "coqidetop" "" "\n\ +let coqidetop_specific_usage = Usage.{ + executable_name = "coqidetop"; + extra_args = ""; + extra_options = "\n\ coqidetop specific options:\n\ \n --xml_formatinclude dir (idem)\ \n --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ \n --help-XML-protocol print documentation of the Coq XML protocol\n" +} let islave_parse ~opts extra_args = let open Coqtop in @@ -582,7 +586,7 @@ let () = let open Coqtop in let custom = { parse_extra = islave_parse ; - help = Usage.print_usage "coqidetop"; + help = coqidetop_specific_usage; init = islave_init; run = loop; opts = islave_default_opts } in |