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)