# HG changeset patch
# User wenzelm
# Date 1699525833 -3600
# Node ID 0481c84f6919fbb05a69717780c064663d10035a
# Parent  ab85d87dc2beb7649640d72b92be24a9bc606918
proper local host (amending 62d7ef1da441);

diff -r ab85d87dc2be -r 0481c84f6919 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Nov 08 21:45:02 2023 +0100
+++ b/src/Pure/General/ssh.scala	Thu Nov 09 11:30:33 2023 +0100
@@ -432,7 +432,7 @@
     port: Int = 0,
     user: String = ""
   ): System = {
-    if (host.isEmpty) Local
+    if (is_local(host)) Local
     else open_session(options, host = host, port = port, user = user)
   }