# HG changeset patch # User Fabian Huch # Date 1719934708 -7200 # Node ID 59e088605d490a9431946ad91197e01c7ffb9e97 # Parent c766be851bc25e600a82c4b0c8302782f265fe7e only consider jobs late if they have ancestors (amending 12901c03b416); diff -r c766be851bc2 -r 59e088605d49 src/Pure/Build/build_schedule.scala --- a/src/Pure/Build/build_schedule.scala Tue Jul 02 16:42:13 2024 +0200 +++ b/src/Pure/Build/build_schedule.scala Tue Jul 02 17:38:28 2024 +0200 @@ -1156,9 +1156,8 @@ (for { host <- _host_infos.hosts if !active_hosts0.contains(host.name) - jobs = _schedule.next(host.name, state) - ancestors = build_context.sessions_structure.build_requirements(jobs) - if ancestors.forall(ancestor => + ancestors = _schedule.next(host.name, state).flatMap(_schedule.graph.imm_preds) + if ancestors.nonEmpty && ancestors.forall(ancestor => completed_since(ancestor) > build_options.seconds("build_schedule_inactive_delay")) } yield host).toSet