more robust;
authorwenzelm
Fri, 16 Feb 2024 20:19:01 +0100
changeset 79635 8d2539a13502
parent 79634 432217a1e990
child 79636 b3febd2a4c73
more robust;
src/Pure/General/ssh.scala
--- 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)
   }