merged

--- a/src/Pure/Tools/build_schedule.scala	Mon Dec 11 21:31:58 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Mon Dec 11 21:56:24 2023 +0100
@@ -517,8 +517,9 @@
 
         val host_preds =
           for {
-            (name, (node, _)) <- finished.graph.iterator.toSet
-            if node.node_info.hostname == job.node_info.hostname
+            (name, (pred_node, _)) <- finished.graph.iterator.toSet
+            if pred_node.node_info.hostname == job.node_info.hostname
+            if pred_node.end.time <= node.start.time
           } yield name
         val build_preds =
           build_state.sessions.graph.imm_preds(job.name).filter(finished.graph.defined)
@@ -1439,7 +1440,11 @@
         val node = graph.get_node(job_name)
         val rect = draw_node(node)
 
-        graph.imm_preds(job_name).foreach(pred => draw_arrow(graph.get_node(pred), rect))
+        for {
+          pred <- graph.imm_preds(job_name).iterator
+          pred_node = graph.get_node(pred)
+          if node.node_info.hostname != pred_node.node_info.hostname
+        } draw_arrow(pred_node, rect)
       }
     }