# HG changeset patch
# User wenzelm
# Date 1663856222 -7200
# Node ID d535db35388ef97c74b2b6f5ea5bb289db9bbbc5
# Parent  9d1819c28f67b79c9ac956e7c434438b9f3542d6
proper filter (amending fb4215da4919);

diff -r 9d1819c28f67 -r d535db35388e src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Sep 22 14:14:45 2022 +0200
+++ b/src/Pure/Tools/build.scala	Thu Sep 22 16:17:02 2022 +0200
@@ -149,8 +149,7 @@
         foldLeft(Process_Result.RC.ok)(_ max _)
     def ok: Boolean = rc == Process_Result.RC.ok
 
-    def unfinished: List[String] =
-      sessions.iterator.filterNot(name => !apply(name).ok).toList.sorted
+    def unfinished: List[String] = sessions.iterator.filterNot(apply(_).ok).toList.sorted
 
     override def toString: String = rc.toString
   }