# HG changeset patch # User Fabian Huch # Date 1738445312 -3600 # Node ID 0dc7b3253aaaafd9a3261056d2490da65d82688c # Parent e0ba5e9850df0f2fbbe62e95679a8af7bd7cf0ec clarified options: extra ssh connection to cluster of build_manager; diff -r e0ba5e9850df -r 0dc7b3253aaa etc/options --- a/etc/options Sat Feb 01 22:20:42 2025 +0100 +++ b/etc/options Sat Feb 01 22:28:32 2025 +0100 @@ -495,6 +495,10 @@ option build_manager_ssh_port : int = 0 for connection +option build_manager_cluster_ssh_host : string = "localhost" for connection +option build_manager_cluster_ssh_user : string = "" for connection +option build_manager_cluster_ssh_port : int = 0 for connection + section "Build Manager Database" diff -r e0ba5e9850df -r 0dc7b3253aaa src/Pure/Build/build_manager.scala --- 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"),