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