# HG changeset patch
# User wenzelm
# Date 1663187046 -7200
# Node ID e73025785dc7808c8f7b3b6a072a99383751ae79
# Parent  6149f7553ea9882f9f786d3db48d3248e49438e1
tuned message;

diff -r 6149f7553ea9 -r e73025785dc7 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 =