tuned message: failure may stem from build_cluster init;
authorwenzelm
Tue, 22 Aug 2023 13:27:53 +0200
changeset 78566 a04277e3b313
parent 78565 05de3e068312
child 78567 db99a70f8531
tuned message: failure may stem from build_cluster init;
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))
         }