# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1702033882 -3600
# Node ID 8cb732d7a98cb56581384a791e997cb86c523143
# Parent  a22440b9cb70cff3f899440edb294362aa1eb354
tuned;

diff -r a22440b9cb70 -r 8cb732d7a98c src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Dec 07 11:34:01 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Dec 08 12:11:22 2023 +0100
@@ -930,22 +930,19 @@
     }
 
     override def next_jobs(state: Build_Process.State): List[String] = {
-      val finalize_limit = if (build_context.master) Int.MaxValue else 0
-
-      if (progress.stopped) state.next_ready.map(_.name).take(finalize_limit)
-      else if (_schedule.is_current(state)) _schedule.next(hostname, state)
+      if (!progress.stopped && _schedule.is_current(state)) _schedule.next(hostname, state)
+      else if (!build_context.master) Nil
+      else if (progress.stopped) state.next_ready.map(_.name)
       else {
         val current = state.next_ready.filter(task => is_current(state, task.name))
-        if (current.nonEmpty) current.map(_.name).take(finalize_limit)
-        else if (!build_context.master) Nil
+        if (current.nonEmpty) current.map(_.name)
         else {
           val start = Time.now()
           val schedule = scheduler.build_schedule(state)
           val elapsed = Time.now() - start
 
           val timing_msg = if (elapsed.is_relevant) " (took " + elapsed.message + ")" else ""
-          progress.echo_if(build_context.master && !schedule.is_current_estimate(_schedule),
-            schedule.message + timing_msg)
+          progress.echo_if(!_schedule.is_current_estimate(schedule), schedule.message + timing_msg)
 
           _schedule = schedule
           _schedule.next(hostname, state)