filter hosts properly;
authorFabian Huch <huch@in.tum.de>
Thu, 30 Nov 2023 13:44:21 +0100
changeset 79083 2d18d481c115
parent 79082 722937a213ef
child 79084 dd689c4ab688
filter hosts properly;
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