src/Pure/General/mercurial.scala

--- a/src/Pure/General/mercurial.scala	Sat May 25 17:22:05 2024 +0200
+++ b/src/Pure/General/mercurial.scala	Sat May 25 19:42:09 2024 +0200
@@ -126,13 +126,15 @@
     val PATH_DIFF: Path = PATH + Path.explode("diff")
     val PATH_STAT: Path = PATH + Path.explode("stat")
 
+    def ok(root: Path, ssh: SSH.System = SSH.Local): Boolean = ssh.is_dir(root + PATH)
+
     def check_directory(root: Path, ssh: SSH.System = SSH.Local): Unit =
-      if (ssh.is_dir(root) && !ssh.is_dir(root + PATH) && ssh.read_dir(root).nonEmpty) {
+      if (ssh.is_dir(root) && !ok(root, ssh = ssh) && ssh.read_dir(root).nonEmpty) {
         error("No .hg_sync meta data in " + ssh.rsync_path(root))
       }
 
     def directory(root: Path, ssh: SSH.System = SSH.Local): Directory = {
-      if (ssh.is_dir(root + PATH)) new Directory(root, ssh)
+      if (ok(root, ssh = ssh)) new Directory(root, ssh)
       else error("No .hg_sync directory found in " + ssh.rsync_path(root))
     }