--- a/src/Pure/Admin/build_release.scala Mon Aug 08 13:33:04 2022 +0200
+++ b/src/Pure/Admin/build_release.scala Mon Aug 08 14:34:09 2022 +0200
@@ -222,17 +222,22 @@
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
- local_dir: Path
+ local_dir: Path,
+ progress: Progress = new Progress,
): Unit = {
val server_option = "build_host_" + platform.toString
+ val server = options.string(server_option)
+ progress.echo("Building heaps " + commas_quote(build_sessions) +
+ " (" + server_option + " = " + quote(server) + ") ...")
+
val ssh =
- options.string(server_option) match {
+ server match {
case "" =>
if (Platform.family == platform) SSH.Local
else error("Undefined option " + server_option + ": cannot build heaps")
case SSH.Target(user, host) =>
SSH.open_session(options, host = host, user = user)
- case s => error("Malformed option " + server_option + ": " + quote(s))
+ case _ => error("Malformed option " + server_option + ": " + quote(server))
}
try {
Isabelle_System.with_tmp_file("tmp", ext = "tar") { local_tmp_tar =>
@@ -583,8 +588,7 @@
// build heaps
if (build_sessions.nonEmpty) {
- progress.echo("Building heaps " + commas_quote(build_sessions) + " ...")
- build_heaps(options, platform, build_sessions, isabelle_target)
+ build_heaps(options, platform, build_sessions, isabelle_target, progress = progress)
}