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