# HG changeset patch
# User wenzelm
# Date 1663840304 -7200
# Node ID 6bf42525f111e18276a53feb7f3aee99c847c6d1
# Parent  fb4215da4919becf5eb8c79f0e3ce543ae752954
tuned signature;

diff -r fb4215da4919 -r 6bf42525f111 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Sep 22 11:45:30 2022 +0200
+++ b/src/Pure/Tools/build.scala	Thu Sep 22 11:51:44 2022 +0200
@@ -149,6 +149,9 @@
         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
+
     override def toString: String = rc.toString
   }
 
@@ -484,12 +487,7 @@
     }
 
     if (!results.ok && (verbose || !no_build)) {
-      val unfinished =
-        (for {
-          name <- results.sessions.iterator
-          if !results(name).ok
-         } yield name).toList.sorted
-      progress.echo("Unfinished session(s): " + commas(unfinished))
+      progress.echo("Unfinished session(s): " + commas(results.unfinished))
     }
 
     results