# HG changeset patch
# User wenzelm
# Date 1708113254 -3600
# Node ID a14497801192def2528f052c2b8a23196b1ef50a
# Parent  b3febd2a4c7312df60b428a4ac2431a50d681b6d
tuned;

diff -r b3febd2a4c73 -r a14497801192 src/Pure/Build/build_cluster.scala
--- a/src/Pure/Build/build_cluster.scala	Fri Feb 16 20:20:24 2024 +0100
+++ b/src/Pure/Build/build_cluster.scala	Fri Feb 16 20:54:14 2024 +0100
@@ -123,7 +123,7 @@
 
     Path.split(host.dirs)  // check
 
-    def ssh_host: String = proper_string(hostname) getOrElse name
+    def ssh_host: String = proper_string(host.hostname) getOrElse host.name
     def is_local: Boolean = SSH.is_local(ssh_host)
     def is_remote: Boolean = !is_local
 
@@ -150,7 +150,7 @@
 
     def open_ssh(options: Options): SSH.System =
       SSH.open_system(options ++ host.options, ssh_host, port = host.port,
-        user = host.user, user_home = home)
+        user = host.user, user_home = host.home)
 
     def open_session(build_context: Build.Context, progress: Progress = new Progress): Session = {
       val ssh_options = build_context.build_options ++ host.options