src/Pure/Tools/build.ML
changeset 71667 4d2de35214c5
parent 71656 3e121f999120
child 71669 12ebd8d0deee
--- a/src/Pure/Tools/build.ML	Thu Apr 02 13:04:24 2020 +0200
+++ b/src/Pure/Tools/build.ML	Thu Apr 02 20:06:43 2020 +0200
@@ -254,13 +254,16 @@
         let
           val args = decode_args args_yxml;
           val errs =
-            Future.interruptible_task (fn () =>
-              (build_session args; []) handle exn =>
+            Future.interruptible_task (fn () => (build_session args; [])) () handle exn =>
               (Runtime.exn_message_list exn handle _ (*sic!*) =>
                 (build_session_finished ["CRASHED"];
-                  raise Isabelle_Process.EXIT 1))) ();
+                  raise Isabelle_Process.EXIT 2));
           val _ = build_session_finished errs;
-        in if null errs then () else raise Isabelle_Process.EXIT 1 end
+        in
+          if null errs
+          then raise Isabelle_Process.STOP
+          else raise Isabelle_Process.EXIT 1
+        end
       | _ => raise Match);
 
 end;