From f2779d48d3b7735687444e22b16cdb7cb8f7ce60 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 May 2019 09:36:57 +0200
Subject: Usage: bypassing a useless detour via a reference.

---
 ide/idetop.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'ide')

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
-- 
cgit v1.2.3