changeset 72341 | 0973a594be72 |
parent 71973 | 2108c0e7ce13 |
child 72375 | e48d93811ed7 |
--- a/src/Pure/Admin/build_release.scala Tue Sep 29 20:00:59 2020 +0200 +++ b/src/Pure/Admin/build_release.scala Tue Sep 29 20:08:08 2020 +0200 @@ -228,7 +228,7 @@ build_sessions: List[String], local_dir: Path) { - val server_option = "build_release_server_" + platform.toString + val server_option = "build_host_" + platform.toString options.string(server_option) match { case SSH.Target(user, host) => using(SSH.open_session(options, host = host, user = user))(ssh =>