# HG changeset patch
# User wenzelm
# Date 1504126130 -7200
# Node ID 37b16f8af3516c58c77335fdf50d68fc6f3a1e78
# Parent  b17d41779768c997db17336667000a68513cc23e
faster check for non-repository, especially relevant for find_repository to avoid repeated invocation of "hg root";

diff -r b17d41779768 -r 37b16f8af351 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Wed Aug 30 20:50:45 2017 +0200
+++ b/src/Pure/General/mercurial.scala	Wed Aug 30 22:48:50 2017 +0200
@@ -29,7 +29,15 @@
   /* repository access */
 
   def is_repository(root: Path, ssh: Option[SSH.Session] = None): Boolean =
-    new Repository(root, ssh).command("root").ok
+  {
+    val root_hg = root + Path.explode(".hg")
+    val root_hg_present =
+      ssh match {
+        case None => root_hg.is_dir
+        case Some(ssh) => ssh.is_dir(root_hg)
+      }
+    root_hg_present && new Repository(root, ssh).command("root").ok
+  }
 
   def repository(root: Path, ssh: Option[SSH.Session] = None): Repository =
   {