# HG changeset patch
# User wenzelm
# Date 1708111141 -3600
# Node ID 8d2539a13502a552ed8ed821f90896a0f099f248
# Parent  432217a1e990d6438bafc1ba26c4e089c36fd449
more robust;

diff -r 432217a1e990 -r 8d2539a13502 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)
   }