tuned;
authorwenzelm
Fri, 16 Feb 2024 20:54:14 +0100
changeset 79637 a14497801192
parent 79636 b3febd2a4c73
child 79638 7eaf1931f408
tuned;
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