author | wenzelm |
Fri, 16 Feb 2024 20:19:01 +0100 | |
changeset 79635 | 8d2539a13502 |
parent 79634 | 432217a1e990 |
child 79636 | b3febd2a4c73 |
--- a/src/Pure/General/ssh.scala Fri Feb 16 20:18:21 2024 +0100 +++ b/src/Pure/General/ssh.scala Fri Feb 16 20:19:01 2024 +0100 @@ -450,7 +450,10 @@ user: String = "", user_home: String = "" ): System = { - if (is_local(host)) Local + if (is_local(host)) { + if (user_home.isEmpty) Local + else error("Illegal user home for local host") + } else open_session(options, host = host, port = port, user = user, user_home = user_home) }