# HG changeset patch
# User wenzelm
# Date 1497707071 -7200
# Node ID 5aab14a64a033c54222a9a967dc64d7042f433b2
# Parent  8ff7fd4ee9197edc0d0da8b3dfda8ba9a51b3939
tuned signature;

diff -r 8ff7fd4ee919 -r 5aab14a64a03 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Jun 17 14:52:23 2017 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Jun 17 15:44:31 2017 +0200
@@ -51,15 +51,16 @@
     }
   }
 
-  def clone_repository(
-    source: String, root: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository =
+  def clone_repository(source: String, root: Path, rev: String = "", options: String = "",
+    ssh: Option[SSH.Session] = None): Repository =
   {
     val hg = new Repository(root, ssh)
     ssh match {
       case None => Isabelle_System.mkdirs(hg.root.dir)
       case Some(ssh) => ssh.mkdirs(hg.root.dir)
     }
-    hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root), options).check
+    hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root) + opt_rev(rev), options)
+      .check
     hg
   }