tuned message;
authorwenzelm
Wed, 14 Sep 2022 22:24:06 +0200
changeset 76156 e73025785dc7
parent 76155 6149f7553ea9
child 76157 ff404465b20d
tuned message;
src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed Sep 14 21:50:38 2022 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Sep 14 22:24:06 2022 +0200
@@ -227,7 +227,7 @@
   ): Unit = {
     val server_option = "build_host_" + platform.toString
     val server = options.string(server_option)
-    progress.echo("Building heaps " + commas_quote(build_sessions) +
+    progress.echo("Building heaps for " + commas_quote(build_sessions) +
       " (" + server_option + " = " + quote(server) + ") ...")
 
     val ssh =