--- a/src/Pure/Tools/build_schedule.scala Thu Nov 09 11:41:19 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala Thu Nov 09 11:49:08 2023 +0100
@@ -553,7 +553,9 @@
}
override def next_jobs(state: Build_Process.State): List[String] =
- if (cache.is_current(state)) cache.configs.map(_.job_name)
+ if (progress.stopped)
+ state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name)).map(_.name)
+ else if (cache.is_current(state)) cache.configs.map(_.job_name)
else {
val start = Time.now()
val next = scheduler.next(state)