# HG changeset patch
# User wenzelm
# Date 1477040416 -7200
# Node ID d9a9ae3956f65b5f9e5db487ace3397632269359
# Parent  8f9d27c89241db20890f00284f50058feb3f8bb1
more operations;

diff -r 8f9d27c89241 -r d9a9ae3956f6 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Thu Oct 20 20:03:32 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Fri Oct 21 11:00:16 2016 +0200
@@ -25,6 +25,9 @@
 
   /* repository access */
 
+  def is_repository(root: Path, ssh: Option[SSH.Session] = None): Boolean =
+    new Repository(root, ssh).command("root").ok
+
   def repository(root: Path, ssh: Option[SSH.Session] = None): Repository =
   {
     val hg = new Repository(root, ssh)