faster check for non-repository, especially relevant for find_repository to avoid repeated invocation of "hg root";
authorwenzelm
Wed, 30 Aug 2017 22:48:50 +0200
changeset 66558 37b16f8af351
parent 66557 b17d41779768
child 66559 beb48215cda7
faster check for non-repository, especially relevant for find_repository to avoid repeated invocation of "hg root";
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 =
   {