diff -r c8537bef99eb -r f6a9271cb177 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Mon Jul 08 17:44:20 2024 +0200
+++ b/src/Pure/Build/build.scala	Mon Jul 08 17:57:19 2024 +0200
@@ -691,17 +691,14 @@
         else if (quiet) new Progress
         else new Console_Progress(verbose = verbose)
 
-      val results =
-        progress.interrupt_handler {
-          build_worker(options,
-            build_id = build_id,
-            progress = progress,
-            dirs = dirs.toList,
-            numa_shuffling = Host.numa_check(progress, numa_shuffling),
-            max_jobs = max_jobs)
-        }
-
-      if (!results.ok) sys.exit(results.rc)
+      progress.interrupt_handler {
+        build_worker(options,
+          build_id = build_id,
+          progress = progress,
+          dirs = dirs.toList,
+          numa_shuffling = Host.numa_check(progress, numa_shuffling),
+          max_jobs = max_jobs)
+      }
     })