# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1710942976 -3600
# Node ID 05e034a5492409a40ea11069a97e59781c215821
# Parent  ca004ccf2352c6702e2f40513209d7346f09f946
only start jobs early if they are due (cf. 1966578feff8);

diff -r ca004ccf2352 -r 05e034a54924 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Thu Mar 21 14:19:39 2024 +0000
+++ b/src/Pure/Build/build_schedule.scala	Wed Mar 20 14:56:16 2024 +0100
@@ -573,6 +573,8 @@
       else elapsed() > options.seconds("build_schedule_outdated_delay")
 
     def next(hostname: String, state: Build_Process.State): List[String] = {
+      val now = Time.now()
+
       val next_nodes =
         for {
           task <- state.next_ready
@@ -581,8 +583,10 @@
           if hostname == node.node_info.hostname
         } yield node
 
-      val (ready, waiting) =
+      val (ready, other) =
         next_nodes.partition(node => graph.imm_preds(node.job_name).subsetOf(state.results.keySet))
+
+      val waiting = other.filter(_.start.time <= now)
       val running = state.running.values.toList.map(_.node_info).filter(_.hostname == hostname)
 
       def try_run(ready: List[Schedule.Node], next: Schedule.Node): List[Schedule.Node] = {