src/Pure/General/ssh.scala
changeset 71562 794c8b0ad8f1
parent 71549 319599ba28cf
child 71564 03133befa33b
--- 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)