--- 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)
+ }
})