# HG changeset patch
# User wenzelm
# Date 1663056713 -7200
# Node ID 2bb6eb6df6c2b7490176655f86d930712124de53
# Parent  8b695e59db3fefd89d3bee0c7b17c43d2e44104d
proper port for Mercurial;

diff -r 8b695e59db3f -r 2bb6eb6df6c2 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Sep 13 09:59:08 2022 +0200
+++ b/src/Pure/General/ssh.scala	Tue Sep 13 10:11:53 2022 +0200
@@ -107,7 +107,7 @@
     ssh =>
 
     override def toString: String = user_prefix(user) + host + port_suffix(port)
-    override def hg_url: String = "ssh://" + user_prefix(user) + host + "/"
+    override def hg_url: String = "ssh://" + toString + "/"
     override def rsync_prefix: String = user_prefix(user) + host + ":"