tuned;
authorwenzelm
Thu, 31 Aug 2017 11:15:38 +0200
changeset 66569 1a475e59c70f
parent 66566 a14bbbaa628d
child 66570 9af879e222cc
tuned;
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 =