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