--- a/src/Pure/Build/build_manager.scala Sat Feb 01 22:20:42 2025 +0100
+++ b/src/Pure/Build/build_manager.scala Sat Feb 01 22:28:32 2025 +0100
@@ -1537,7 +1537,7 @@
if (task.build_cluster) store.options.string("build_cluster_identifier") else store.identifier
def open_ssh(): SSH.System = {
- if (task.build_cluster) store.open_ssh()
+ if (task.build_cluster) store.open_cluster_ssh()
else Library.the_single(task.build_hosts).open_ssh(store.options)
}
}
@@ -1637,6 +1637,12 @@
val ssh_group: String = options.string("build_manager_ssh_group")
+ def open_cluster_ssh(): SSH.Session =
+ SSH.open_session(options,
+ host = options.string("build_manager_cluster_ssh_host"),
+ port = options.int("build_manager_cluster_ssh_port"),
+ user = options.string("build_manager_cluster_ssh_user"))
+
def open_ssh(): SSH.Session =
SSH.open_session(options,
host = options.string("build_manager_ssh_host"),