--- 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 +