# HG changeset patch
# User wenzelm
# Date 1476630624 -7200
# Node ID a9f5408816118aef5fa2353672f7cb04cc9fe6aa
# Parent  b1aef25ce8dfe86021339b5033d0f51657d953f1
more robust;

diff -r b1aef25ce8df -r a9f540881611 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sun Oct 16 16:58:09 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Sun Oct 16 17:10:24 2016 +0200
@@ -35,6 +35,10 @@
     source: String, root: Path, 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(session) => using(session.sftp())(_.mkdirs(hg.root.dir))
+    }
     hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check
     hg
   }