proper filter for approximations;
authorFabian Huch <huch@in.tum.de>
Fri, 24 Nov 2023 12:35:00 +0100
changeset 79034 30411c1c575d
parent 79033 83288e02c6fa
child 79035 6beb60b508e6
proper filter for approximations;
src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Fri Nov 24 10:36:23 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Nov 24 12:35:00 2023 +0100
@@ -54,8 +54,8 @@
 
     def approximate_threads(threads: Int): Option[Time] = {
       val approximations =
-        by_job.values.filter(_.size > 1).map { data =>
-          val (ref_hostname, x0) =
+        by_job.values.filter(_.by_threads.size > 1).map { data =>
+          val (ref_hostname, _) =
             data.by_hostname.toList.flatMap((hostname, data) =>
               data.by_threads.keys.map(hostname -> _)).minBy((_, n) => Math.abs(n - threads))