src/Pure/General/ssh.scala
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)
   }