diff -r 0e79fa88cab6 -r d637e60427db src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Aug 16 14:42:43 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Aug 16 14:50:17 2023 +0200
@@ -55,7 +55,7 @@
     build: Option[Build_Job]
   ) extends Library.Named {
     def no_build: Job = copy(build = None)
-    def join_build: Option[(Process_Result, SHA1.Shasum)] = build.flatMap(_.join)
+    def join_build: Option[Build_Job.Result] = build.flatMap(_.join)
   }
 
   sealed case class Result(
@@ -1142,12 +1142,14 @@
               job.join_build match {
                 case None =>
                   _state = _state.remove_running(job.name)
-                case Some((process_result, output_shasum)) =>
+                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, process_result, output_shasum,
+                    make_result(result_name,
+                      result.process_result,
+                      result.output_shasum,
                       node_info = job.node_info)
               }
             }