tuned signature;

--- 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