# HG changeset patch
# User wenzelm
# Date 1699536139 -3600
# Node ID 35d42112301a0ca4af4c11ab922f17f2b2171dfe
# Parent  b33a7c6b99c5e60c57b276b4900b79fd7fcdb9c4
clarified signature: more operations;

diff -r b33a7c6b99c5 -r 35d42112301a src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Thu Nov 09 13:31:09 2023 +0100
+++ b/src/Pure/Tools/build_cluster.scala	Thu Nov 09 14:22:19 2023 +0100
@@ -126,10 +126,13 @@
 
     def message(msg: String): String = "Host " + quote(host.name) + if_proper(msg, ": " + msg)
 
+    def open_ssh(options: Options): SSH.System =
+      SSH.open_system(options ++ host.options, ssh_host, port = host.port, user = host.user)
+
     def open_session(build_context: Build.Context, progress: Progress = new Progress): Session = {
-      val session_options = build_context.build_options ++ host.options
-      val ssh = SSH.open_session(session_options, ssh_host, port = host.port, user = host.user)
-      new Session(build_context, host, session_options, ssh, progress)
+      val ssh_options = build_context.build_options ++ host.options
+      val ssh = open_ssh(build_context.build_options)
+      new Session(build_context, host, ssh_options, ssh, progress)
     }
   }