--- 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))