--- 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)