# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1699549101 -3600
# Node ID 4f940d7293ea2615ed662b38af5a874ce96a55ae
# Parent  ae1403e341dd337ec63c91c76b6fe945f082c71a
use only finished sessions in timing data;

diff -r ae1403e341dd -r 4f940d7293ea src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 09 16:39:36 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Nov 09 17:58:21 2023 +0100
@@ -143,6 +143,7 @@
           (meta_info, build_info) <- build_history
           build_host <- meta_info.get(Build_Log.Prop.build_host).toList
           (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
           threads = session_info.threads.getOrElse(host.info.num_cpus)