# HG changeset patch
# User wenzelm
# Date 1710342863 -3600
# Node ID 70d4dcede0dc680c69d0810a51629c3b31726693
# Parent  caf61c098754624a7889ff07b6e0698aca560df7
tuned;

diff -r caf61c098754 -r 70d4dcede0dc src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Wed Mar 13 16:09:11 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Wed Mar 13 16:14:23 2024 +0100
@@ -233,7 +233,7 @@
     def next_serial: Long = State.inc_serial(serial)
 
     def ready: List[Task] = pending.valuesIterator.filter(_.is_ready).toList.sortBy(_.name)
-    def next_ready: List[Task] = ready.filter(entry => !is_running(entry.name))
+    def next_ready: List[Task] = ready.filter(task => !is_running(task.name))
 
     def remove_pending(a: String): State =
       copy(pending =