# HG changeset patch
# User wenzelm
# Date 1716991083 -7200
# Node ID f0ead4febf7f264aaa205d7eae14b2ba11209080
# Parent  f2fa6753c3e2e6be9bbd2c355f85880cfd7b1489
tuned;

diff -r f2fa6753c3e2 -r f0ead4febf7f src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed May 29 15:51:15 2024 +0200
+++ b/src/Pure/General/ssh.scala	Wed May 29 15:58:03 2024 +0200
@@ -123,7 +123,7 @@
     override def ssh_session: Option[Session] = Some(ssh)
 
     def port_suffix: String = if (port > 0) ":" + port else ""
-    def user_prefix: String = if (user.nonEmpty) user + "@" else ""
+    def user_prefix: String = if_proper(user, user + "@")
 
     override def toString: String = user_prefix + host + port_suffix
     override def print: String = " (ssh " + toString + ")"