diff options
| author | Gaëtan Gilbert | 2019-02-08 13:34:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-08 13:34:02 +0100 |
| commit | 6c06f36b2dd1812454d40cbde1da28e1ea8be67e (patch) | |
| tree | 62782d00b4c5781caf89dfc08e804f220e6cc790 /checker | |
| parent | 99c1d7b0ae1beed66fe8dd6a06db84dc0c8322d8 (diff) | |
Make boot flag into a normal option (no global flag).
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checker.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index d97ab5409e..af8d1e5617 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -319,6 +319,8 @@ let explain_exn = function let deprecated flag = Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag)) +let boot_opt = ref false + let parse_args argv = let rec parse = function | [] -> () @@ -348,14 +350,14 @@ let parse_args argv = | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); + Envars.set_coqlib ~boot:!boot_opt ~fail:(fun x -> CErrors.user_err Pp.(str x)); print_endline (Envars.coqlib ()); exit 0 | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - | "-boot" :: rem -> Flags.boot := true; parse rem + | "-boot" :: rem -> boot_opt := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem @@ -384,7 +386,7 @@ let init_with_argv argv = try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; - Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); + Envars.set_coqlib ~boot:!boot_opt ~fail:(fun x -> CErrors.user_err Pp.(str x)); Flags.if_verbose print_header (); init_load_path (); make_senv () |