src/Pure/Tools/build_schedule.scala
changeset 79191 ee405c40db72
parent 79190 2039f3609884
child 79192 5db03f9276e2
--- a/src/Pure/Tools/build_schedule.scala	Fri Dec 08 15:21:51 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Dec 08 17:00:13 2023 +0100
@@ -464,8 +464,8 @@
       for {
         task <- state.next_ready
         node = graph.get_node(task.name)
-        if node.start.time == start.time
         if hostname == node.node_info.hostname
+        if graph.imm_preds(node.job_name).subsetOf(state.results.keySet)
       } yield task.name
   }
 
@@ -491,10 +491,16 @@
         val now = current_time + elapsed
         val node = Schedule.Node(job.name, job.node_info, job.start_date, now - job.start_date.time)
 
-        val preds =
+        val host_preds =
+          for {
+            (name, (node, _)) <- finished.graph.iterator.toSet
+            if node.node_info.hostname == job.node_info.hostname
+          } yield name
+        val build_preds =
           build_state.sessions.graph.imm_preds(job.name).filter(finished.graph.defined)
-        val graph =
-          preds.foldLeft(finished.graph.new_node(job.name, node))(_.add_edge(_, job.name))
+        val preds = build_preds ++ host_preds
+
+        val graph = preds.foldLeft(finished.graph.new_node(job.name, node))(_.add_edge(_, job.name))
 
         val build_state1 = build_state.remove_running(job.name).remove_pending(job.name)
         State(build_state1, now, finished.copy(graph = graph))