# HG changeset patch
# User wenzelm
# Date 1678786037 -3600
# Node ID 739cb777cc758d2e1a8adc627c805332c62911c9
# Parent  e79a5ce8a74c4f5c9b1cb80dbd577fd4492391c6
clarified signature;

diff -r e79a5ce8a74c -r 739cb777cc75 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Tue Mar 14 10:16:45 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Tue Mar 14 10:27:17 2023 +0100
@@ -11,7 +11,6 @@
 
 
 trait Build_Job {
-  def node_info: Host.Node_Info
   def cancel(): Unit = ()
   def is_finished: Boolean = false
   def join: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum)
@@ -103,7 +102,7 @@
     log: Logger,
     session_background: Sessions.Background,
     input_shasum: SHA1.Shasum,
-    override val node_info: Host.Node_Info
+    node_info: Host.Node_Info
   ) extends Build_Job {
     private val store = build_context.store
 
diff -r e79a5ce8a74c -r 739cb777cc75 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Mar 14 10:16:45 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Mar 14 10:27:17 2023 +0100
@@ -248,10 +248,10 @@
     def stop_running(): Unit =
       for (job <- running.valuesIterator; build <- job.build) build.cancel()
 
-    def finished_running(): List[(String, Build_Job)] =
+    def finished_running(): List[Job] =
       List.from(
         for (job <- running.valuesIterator; build <- job.build if build.is_finished)
-        yield job.name -> build)
+        yield job)
 
     def add_running(job: Job): State =
       copy(running = running + (job.name -> job))
@@ -1066,12 +1066,12 @@
           synchronized_database {
             if (progress.stopped) _state.stop_running()
 
-            for ((job_name, build) <- _state.finished_running()) {
-              val (process_result, output_shasum) = build.join
+            for (job <- _state.finished_running()) {
+              val (process_result, output_shasum) = job.build.get.join
               _state = _state.
-                remove_pending(job_name).
-                remove_running(job_name).
-                make_result(job_name, process_result, output_shasum, node_info = build.node_info)
+                remove_pending(job.name).
+                remove_running(job.name).
+                make_result(job.name, process_result, output_shasum, node_info = job.node_info)
             }
           }