tuned;
authorwenzelm
Wed, 13 Mar 2024 16:14:23 +0100
changeset 79885 70d4dcede0dc
parent 79884 caf61c098754
child 79886 7ae25372ab04
tuned;
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 =