improve graphical clarity by omitting intra-host dependencies (following ee405c40db72);
--- a/src/Pure/Tools/build_schedule.scala Sun Dec 10 18:27:53 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala Mon Dec 11 16:49:26 2023 +0100
@@ -1439,7 +1439,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)
}
}