# HG changeset patch
# User wenzelm
# Date 1693753003 -7200
# Node ID ffa417b5c9137255818c24137df05f49a3af1b8d
# Parent  5ee978b3c00967e850675eb53f0f88da2d78dfbe
tuned;

diff -r 5ee978b3c009 -r ffa417b5c913 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Sep 03 16:47:54 2023 +0200
+++ b/src/Pure/Tools/build.scala	Sun Sep 03 16:56:43 2023 +0200
@@ -475,10 +475,7 @@
         case Some(db) => " (database " + db + ")"
       }
     if (builds.isEmpty) "No build processes" + print_database
-    else {
-      "Build processes" + print_database +
-        (for (build <- builds.iterator) yield "\n  " + build.print).mkString
-    }
+    else "Build processes" + print_database + builds.map(build => "\n  " + build.print).mkString
   }
 
   def find_builds(