proper SSH.System operation;
authorwenzelm
Fri, 24 May 2024 17:14:02 +0200
changeset 80190 9f3e0d98fbec
parent 80189 e8d4ac2f21ea
child 80191 c934f0e51f1c
proper SSH.System operation;
src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Fri May 24 17:06:57 2024 +0200
+++ b/src/Pure/General/mercurial.scala	Fri May 24 17:14:02 2024 +0200
@@ -168,7 +168,7 @@
     for (hg <- detect_repository(root, ssh = ssh)) yield hg.id(rev = rev)
 
   def repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
-    detect_repository(root, ssh = ssh) getOrElse error("Bad hg repository " + root.expand)
+    detect_repository(root, ssh = ssh) getOrElse error("Bad hg repository " + ssh.expand_path(root))
 
   def self_repository(): Repository = repository(Path.ISABELLE_HOME)