--- a/src/Pure/General/mercurial.scala Sat Oct 22 17:27:27 2016 +0200
+++ b/src/Pure/General/mercurial.scala Sat Oct 22 19:14:38 2016 +0200
@@ -68,6 +68,12 @@
case Some(ssh) => root_path.expand_env(ssh.settings)
}
+ def root_url: String =
+ ssh match {
+ case None => root.implode
+ case Some(ssh) => ssh.hg_url + root.implode
+ }
+
override def toString: String =
ssh match {
case None => root.implode
--- a/src/Pure/General/ssh.scala Sat Oct 22 17:27:27 2016 +0200
+++ b/src/Pure/General/ssh.scala Sat Oct 22 19:14:38 2016 +0200
@@ -226,11 +226,13 @@
{
def update_options(new_options: Options): Session = new Session(new_options, session)
+ def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@"
+ def host: String = if (session.getHost == null) "" else session.getHost
+ def port_suffix: String = if (session.getPort == default_port) "" else ":" + session.getPort
+ def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/"
+
override def toString: String =
- (if (session.getUserName == null) "" else session.getUserName + "@") +
- (if (session.getHost == null) "" else session.getHost) +
- (if (session.getPort == default_port) "" else ":" + session.getPort) +
- (if (session.isConnected) "" else " (disconnected)")
+ user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)")
/* sftp channel */