# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# 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"),