diff options
| author | Xavier Clerc | 2014-11-14 17:05:36 +0100 |
|---|---|---|
| committer | Xavier Clerc | 2014-11-14 17:05:36 +0100 |
| commit | 78793236fa289d6e48cb10c9694ee493e0952c28 (patch) | |
| tree | a06c5009effe9fb9888fcb30b13da658082a2347 /checker | |
| parent | 158d4815493db425ddeddcaa7e8448368c9e818f (diff) | |
Exit with code 129 when an anomaly occurs.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checker.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index b39fc2af74..cb13817ee9 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -16,8 +16,9 @@ open Check let () = at_exit flush_all -let fatal_error info = - flush_all (); pperrnl info; flush_all (); exit 1 +let fatal_error info anomaly = + flush_all (); pperrnl info; flush_all (); + exit (if anomaly then 129 else 1) let coq_root = Id.of_string "Coq" let parse_dir s = @@ -323,7 +324,7 @@ let parse_args argv = | "-coqlib" :: s :: rem -> if not (exists_dir s) then - fatal_error (str ("Directory '"^s^"' does not exist")); + fatal_error (str ("Directory '"^s^"' does not exist")) false; Flags.coqlib := s; Flags.coqlib_spec := true; parse rem @@ -363,7 +364,7 @@ let parse_args argv = Flags.make_silent true; parse rem | s :: _ when s<>"" && s.[0]='-' -> - fatal_error (str "Unknown option " ++ str s) + fatal_error (str "Unknown option " ++ str s) false | s :: rem -> add_compile s; parse rem in parse (List.tl (Array.to_list argv)) @@ -384,7 +385,7 @@ let init_with_argv argv = init_load_path (); engage (); with e -> - fatal_error (str "Error during initialization :" ++ (explain_exn e)) + fatal_error (str "Error during initialization :" ++ (explain_exn e)) (is_anomaly e) end let init() = init_with_argv Sys.argv @@ -395,6 +396,6 @@ let run () = flush_all() with e -> if !Flags.debug then Printexc.print_backtrace stderr; - fatal_error (explain_exn e) + fatal_error (explain_exn e) (is_anomaly e) let start () = init(); run(); Check_stat.stats(); exit 0 |