# HG changeset patch
# User wenzelm
# Date 1680965960 -7200
# Node ID 3badbb7bc7ed54c59e6428773043b2d67843189c
# Parent  721b3278c8e47c7eb2b4374dd1e07b8dca3a3383
tuned signature;

diff -r 721b3278c8e4 -r 3badbb7bc7ed src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Apr 08 16:58:01 2023 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Apr 08 16:59:20 2023 +0200
@@ -131,11 +131,8 @@
         error("No .hg_sync meta data in " + ssh.rsync_path(root))
       }
 
-    def is_directory(root: Path, ssh: SSH.System = SSH.Local): Boolean =
-      ssh.is_dir(root + PATH)
-
     def directory(root: Path, ssh: SSH.System = SSH.Local): Directory = {
-      if (is_directory(root, ssh = ssh)) new Directory(root, ssh)
+      if (ssh.is_dir(root + PATH)) new Directory(root, ssh)
       else error("No .hg_sync directory found in " + ssh.rsync_path(root))
     }