tuned output;
authorwenzelm
Wed, 28 Jun 2023 12:30:30 +0200
changeset 78225 5da972859ea6
parent 78224 d85d0d41b2bd
child 78226 73be8ec88721
tuned output;
src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Jun 28 12:25:54 2023 +0200
+++ b/src/Pure/Tools/build.scala	Wed Jun 28 12:30:30 2023 +0200
@@ -390,11 +390,11 @@
       val print_database =
         build_database match {
           case None => ""
-          case Some(db) => " (database " + db + ")"
+          case Some(db) => " (database: " + db + ")"
         }
       if (builds.isEmpty) "No build processes available" + print_database
       else {
-        "Available build processes" + print_database + ":" +
+        "Available build processes" + print_database +
           (for ((build, i) <- builds.iterator.zipWithIndex)
             yield {
               "\n  " + (i + 1) + ": " + build.build_uuid +