# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1703007065 -3600
# Node ID ae0a2cb42b05f252cb1596a409d7ef5c7e45ab41
# Parent  1f694e4b2b3aded81fbdb4a145676eb5ac2fffb2
continue build while waiting for updated schedule;

diff -r 1f694e4b2b3a -r ae0a2cb42b05 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Tue Dec 19 18:28:35 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Tue Dec 19 18:31:05 2023 +0100
@@ -861,8 +861,7 @@
       _schedule.graph.get_node(session_name).node_info
 
     override def next_jobs(state: Build_Process.State): List[String] =
-      if (progress.stopped || _schedule.is_outdated(build_options, state)) Nil
-      else _schedule.next(hostname, state)
+      if (progress.stopped || _schedule.is_empty) Nil else _schedule.next(hostname, state)
   }
 
   abstract class Scheduler_Build_Process(