Exit with code 129 when an anomaly occurs.

2 files changed, 13 insertions, 11 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
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0407fe63c4..35d68603aa 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -20,8 +20,9 @@ let () = at_exit flush_all
 
 let ( / ) = Filename.concat
 
-let fatal_error info =
-  pperrnl info; flush_all (); exit 1
+let fatal_error info anomaly =
+  pperrnl info; flush_all ();
+  exit (if anomaly then 129 else 1)
 
 let get_version_date () =
   try
@@ -476,8 +477,8 @@ let parse_args arglist =
   with
     | UserError(_, s) as e ->
       if is_empty s then exit 1
-      else fatal_error (Errors.print e)
-    | any -> fatal_error (Errors.print any)
+      else fatal_error (Errors.print e) false
+    | any -> fatal_error (Errors.print any) (Errors.is_anomaly any)
 
 let init arglist =
   init_gc ();
@@ -532,7 +533,7 @@ let init arglist =
         if !batch_mode then mt ()
         else str "Error during initialization:" ++ fnl ()
       in
-      fatal_error (msg ++ Coqloop.print_toplevel_error any)
+      fatal_error (msg ++ Coqloop.print_toplevel_error any) (Errors.is_anomaly any)
   end;
   if !batch_mode then begin
     flush_all();