# HG changeset patch
# User wenzelm
# Date 1693752474 -7200
# Node ID 5ee978b3c00967e850675eb53f0f88da2d78dfbe
# Parent  ca56952b732216c3e42c243ed14bb10c06bf9960
tuned messages;

diff -r ca56952b7322 -r 5ee978b3c009 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Sep 03 16:44:07 2023 +0200
+++ b/src/Pure/Tools/build.scala	Sun Sep 03 16:47:54 2023 +0200
@@ -474,9 +474,9 @@
         case None => ""
         case Some(db) => " (database " + db + ")"
       }
-    if (builds.isEmpty) "No build processes available" + print_database
+    if (builds.isEmpty) "No build processes" + print_database
     else {
-      "Available build processes" + print_database +
+      "Build processes" + print_database +
         (for (build <- builds.iterator) yield "\n  " + build.print).mkString
     }
   }