clarified output;
authorwenzelm
Wed, 18 Mar 2020 22:10:29 +0100
changeset 71562 794c8b0ad8f1
parent 71561 1d8b6c2253e6
child 71563 8ddd558d3044
clarified output;
src/Pure/General/mercurial.scala
src/Pure/General/ssh.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 =
--- 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)