# HG changeset patch
# User wenzelm
# Date 1709671492 -3600
# Node ID 3b1ad072d59ad6f1e0071fb3bbc4e9b0d78a1fb4
# Parent  aa03d1a94e3e94754790086af566fd18cf0fcff8
tuned;

diff -r aa03d1a94e3e -r 3b1ad072d59a src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Tue Mar 05 21:26:18 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Tue Mar 05 21:44:52 2024 +0100
@@ -1126,18 +1126,15 @@
 
   protected def main_unsynchronized(): Unit = {
     for (job <- _state.build_running.filter(_.is_finished)) {
-      job.join_build match {
-        case None =>
-          _state = _state.remove_running(job.name)
-        case Some(result) =>
-          val result_name = (job.name, worker_uuid, build_uuid)
-          _state = _state.
-            remove_pending(job.name).
-            remove_running(job.name).
-            make_result(result_name,
-              result.process_result,
-              result.output_shasum,
-              node_info = job.node_info)
+      _state = _state.remove_running(job.name)
+      for (result <- job.join_build) {
+        val result_name = (job.name, worker_uuid, build_uuid)
+        _state = _state.
+          remove_pending(job.name).
+          make_result(result_name,
+            result.process_result,
+            result.output_shasum,
+            node_info = job.node_info)
       }
     }