diff -r 9e5e6e3c83d1 -r e5c3353df22e src/Pure/Admin/build_release.scala --- 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) }