diff -r f2d7f4334cdc -r 3c02ad5a1586 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/Tools/build.ML	Thu Sep 28 14:43:07 2023 +0200
@@ -109,8 +109,12 @@
             else e ();
         in
           exec (fn () =>
-            (Future.interruptible_task (fn () => (build (); (0, []))) () handle exn =>
-              ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
+            (case Exn.capture (Future.interruptible_task build) () of
+              Exn.Res () => (0, [])
+            | Exn.Exn exn =>
+                (case Exn.capture Runtime.exn_message_list exn of
+                  Exn.Res errs => (1, errs)
+                | Exn.Exn _ (*sic!*) => (2, ["CRASHED"])))
           |> let open XML.Encode in pair int (list string) end
           |> single
           |> Output.protocol_message Markup.build_session_finished)