# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1710427599 -3600
# Node ID 4ec26ed6f481ce118a3c404c4cfa7c59296343ee
# Parent  3acbfeec4a95bec9aaa5e1abf8d130adaa612f89
proper check (amending 9aef1d1535ff);

diff -r 3acbfeec4a95 -r 4ec26ed6f481 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Thu Mar 14 14:20:44 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Thu Mar 14 15:46:39 2024 +0100
@@ -260,7 +260,7 @@
         facet.by_job.get(job_name) match {
           case None =>
             // no data for job, use timeout as esimation for single-threaded job on worst host
-            val default_time = sessions_structure(job_name).timeout
+            val default_time = sessions_structure.get(job_name).map(_.timeout).getOrElse(Time.zero)
             if (default_time > Time.zero) {
               val default_host = host_infos.hosts.sorted(host_infos.host_speeds).head
               default_time