# HG changeset patch # User Fabian Huch # 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