| changeset 79635 | 8d2539a13502 |
| parent 79633 | c59231722f10 |
| child 80187 | b8918a5a669e |
--- 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) }