author | wenzelm |
Wed, 14 Sep 2022 22:24:06 +0200 | |
changeset 76156 | e73025785dc7 |
parent 76155 | 6149f7553ea9 |
child 76157 | ff404465b20d |
--- 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 =