unused;
authorFabian Huch <huch@in.tum.de>
Thu, 14 Mar 2024 18:08:42 +0100
changeset 79898 db9a45e05b5b
parent 79897 661fb7db57ca
child 79899 c73a36081b1c
unused;
src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Thu Mar 14 17:27:40 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Thu Mar 14 18:08:42 2024 +0100
@@ -718,10 +718,6 @@
     val minimals: List[Node] = build_graph.minimals
     val maximals: List[Node] = build_graph.maximals
 
-    def all_preds(node: Node): Set[Node] = build_graph.all_preds(List(node)).toSet
-    val maximals_all_preds: Map[Node, Set[Node]] =
-      maximals.map(node => node -> all_preds(node)).toMap
-
     val best_threads: Map[Node, Int] =
       build_graph.keys.map(node => node -> timing_data.best_threads(node, max_threads)).toMap