# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700825700 -3600
# Node ID 30411c1c575d5c977633a442aec7a5d2ca752296
# Parent  83288e02c6faeb5eb6479bc4384304b509ef5f0e
proper filter for approximations;

diff -r 83288e02c6fa -r 30411c1c575d 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))