diff options
| author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2019-12-09 17:49:51 (GMT) |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2019-12-09 17:49:51 (GMT) |
| commit | fa50ef6b47baa0d1c6ec79e6e4ec364fd47393a3 (patch) | |
| tree | 486edb22af8f955634696748764f08b402352fc0 | |
| parent | e176cec9cd3c9264919c8f2e773b608ec3ef2d07 (diff) | |
| parent | 58682be3e6302845d2e3be583c6368510034d767 (diff) | |
| download | coq-fa50ef6b47baa0d1c6ec79e6e4ec364fd47393a3.zip coq-fa50ef6b47baa0d1c6ec79e6e4ec364fd47393a3.tar.gz coq-fa50ef6b47baa0d1c6ec79e6e4ec364fd47393a3.tar.bz2 | |
Merge PR #11255: Fix #11254: "coqtop --version" working even in the middle of an installation process
Ack-by: Zimmi48
Reviewed-by: ejgallego
| -rw-r--r-- | doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 18 |
2 files changed, 15 insertions, 7 deletions
diff --git a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst new file mode 100644 index 0000000..ecc1347 --- /dev/null +++ b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst @@ -0,0 +1,4 @@ +- **Fixed:** + ``coqtop --version`` was broken when called in the middle of an installation process + (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing + `#11254 <https://github.com/coq/coq/pull/11254>`_). diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 309f5b6..46dd693 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -155,12 +155,20 @@ let print_style_tags opts = let () = List.iter iter tags in flush_all () +let init_setup = function + | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); + | Some s -> Envars.set_user_coqlib s + let print_query opts = function | PrintVersion -> Usage.version () | PrintMachineReadableVersion -> Usage.machine_readable_version () - | PrintWhere -> print_endline (Envars.coqlib ()) + | PrintWhere -> + let () = init_setup opts.config.coqlib in + print_endline (Envars.coqlib ()) | PrintHelp h -> Usage.print_usage stderr h - | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs + | PrintConfig -> + let () = init_setup opts.config.coqlib in + Envars.print_config stdout Coq_config.all_src_dirs | PrintTags -> print_style_tags opts.config (** GC tweaking *) @@ -188,10 +196,6 @@ let init_gc () = Gc.minor_heap_size = 33554432; (* 4M *) Gc.space_overhead = 120} -let init_setup = function - | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); - | Some s -> Envars.set_user_coqlib s - let init_process () = (* Coq's init process, phase 1: OCaml parameters, basic structures, and IO @@ -256,11 +260,11 @@ type ('a,'b) custom_toplevel = let init_toplevel custom = let () = init_process () in let opts, customopts = init_parse custom.parse_extra custom.help custom.opts in - let () = init_setup opts.config.coqlib in (* Querying or running? *) match opts.main with | Queries q -> List.iter (print_query opts) q; exit 0 | Run -> + let () = init_setup opts.config.coqlib in let customstate = init_execution opts (custom.init customopts) in opts, customopts, customstate |