# HG changeset patch
# User wenzelm
# Date 1692703673 -7200
# Node ID a04277e3b313956cb50ab40378f3413db740e57f
# Parent  05de3e06831249f6fc33f9a479fb63a9311e866c
tuned message: failure may stem from build_cluster init;

diff -r 05de3e068312 -r a04277e3b313 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Aug 22 12:18:31 2023 +0200
+++ b/src/Pure/Tools/build.scala	Tue Aug 22 13:27:53 2023 +0200
@@ -89,7 +89,7 @@
         Process_Result.RC.merge(results.valuesIterator.map(_.strict.rc)))
     def ok: Boolean = rc == Process_Result.RC.ok
 
-    def unfinished: List[String] = sessions.iterator.filterNot(apply(_).ok).toList.sorted
+    lazy val unfinished: List[String] = sessions.iterator.filterNot(apply(_).ok).toList.sorted
 
     override def toString: String = rc.toString
   }
@@ -277,7 +277,7 @@
             progress = progress, server = server)
         }
 
-        if (!results.ok && (progress.verbose || !no_build)) {
+        if (results.unfinished.nonEmpty && (progress.verbose || !no_build)) {
           progress.echo("Unfinished session(s): " + commas(results.unfinished))
         }