diff options
| author | Emilio Jesus Gallego Arias | 2019-02-08 18:53:55 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-08 18:53:55 +0100 |
| commit | 92df98da23057a47a6cd2053618fd97efe54ba30 (patch) | |
| tree | 1ebc2880fa850e5c095b064972158a940844a85f /checker | |
| parent | 3b9d338c751acd6694038b30e0c40637449df86a (diff) | |
| parent | 6c06f36b2dd1812454d40cbde1da28e1ea8be67e (diff) | |
Merge PR #9523: Make boot flag into a normal option (no global flag).
Ack-by: SkySkimmer
Reviewed-by: ejgallego
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 () |