# HG changeset patch
# User wenzelm
# Date 1504170938 -7200
# Node ID 1a475e59c70fcc4bd5d55081141393ad149746b8
# Parent  a14bbbaa628d40fc0be0c1caa72b31d1e1432a6b
tuned;

diff -r a14bbbaa628d -r 1a475e59c70f src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Thu Aug 31 09:50:11 2017 +0200
+++ b/src/Pure/General/mercurial.scala	Thu Aug 31 11:15:38 2017 +0200
@@ -90,7 +90,7 @@
     val root =
       ssh match {
         case None => root_path.expand
-        case Some(ssh) => root_path.expand_env(ssh.settings)
+        case Some(ssh) => ssh.expand_path(root_path)
       }
 
     def root_url: String =