# HG changeset patch
# User wenzelm
# Date 1584565829 -3600
# Node ID 794c8b0ad8f18edbd900855fbbad183bda43f18d
# Parent  1d8b6c2253e6ae8c1b04775b8ab447d53cca442e
clarified output;

diff -r 1d8b6c2253e6 -r 794c8b0ad8f1 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Mon Mar 16 23:02:55 2020 +0100
+++ b/src/Pure/General/mercurial.scala	Wed Mar 18 22:10:29 2020 +0100
@@ -82,7 +82,7 @@
     val root: Path = ssh.expand_path(root_path)
     def root_url: String = ssh.hg_url + root.implode
 
-    override def toString: String = ssh.prefix + root.implode
+    override def toString: String = ssh.hg_url + root.implode
 
     def command(name: String, args: String = "", options: String = "",
       repository: Boolean = true): Process_Result =
diff -r 1d8b6c2253e6 -r 794c8b0ad8f1 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Mar 16 23:02:55 2020 +0100
+++ b/src/Pure/General/ssh.scala	Wed Mar 18 22:10:29 2020 +0100
@@ -317,9 +317,6 @@
     override def hg_url: String =
       "ssh://" + user_prefix(nominal_user) + nominal_host + "/"
 
-    override def prefix: String =
-      user_prefix(session.getUserName) + host + port_suffix(session.getPort) + ":"
-
     override def toString: String =
       user_prefix(session.getUserName) + host + port_suffix(session.getPort) +
       (if (session.isConnected) "" else " (disconnected)")
@@ -480,7 +477,6 @@
   trait System
   {
     def hg_url: String = ""
-    def prefix: String = ""
 
     def expand_path(path: Path): Path = path.expand
     def bash_path(path: Path): String = File.bash_path(path)