# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1701348261 -3600
# Node ID 2d18d481c1152bea7e561dc88b784f05ac5406de
# Parent  722937a213efddf9e871304d4fe956629e6f0a9b
filter hosts properly;

diff -r 722937a213ef -r 2d18d481c115 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Wed Nov 29 21:29:00 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Nov 30 13:44:21 2023 +0100
@@ -221,11 +221,11 @@
       val measurements =
         for {
           (meta_info, build_info) <- build_history
-          build_host <- meta_info.get(Build_Log.Prop.build_host).toList
+          build_host = meta_info.get(Build_Log.Prop.build_host)
           (job_name, session_info) <- build_info.sessions.toList
           if build_info.finished_sessions.contains(job_name)
-          hostname = session_info.hostname.getOrElse(build_host)
-          host <- hosts.find(_.info.hostname == build_host).toList
+          hostname <- session_info.hostname.orElse(build_host).toList
+          host <- hosts.find(_.info.hostname == hostname).toList
           threads = session_info.threads.getOrElse(host.info.num_cpus)
         } yield (job_name, hostname, threads) -> session_info.timing.elapsed