src/Pure/General/mercurial.scala
changeset 64255 a9f540881611
parent 64252 e84cba30d7ff
child 64256 c3197aeae90b
equal deleted inserted replaced
64254:b1aef25ce8df 64255:a9f540881611
    33 
    33 
    34   def clone_repository(
    34   def clone_repository(
    35     source: String, root: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository =
    35     source: String, root: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository =
    36   {
    36   {
    37     val hg = new Repository(root, ssh)
    37     val hg = new Repository(root, ssh)
       
    38     ssh match {
       
    39       case None => Isabelle_System.mkdirs(hg.root.dir)
       
    40       case Some(session) => using(session.sftp())(_.mkdirs(hg.root.dir))
       
    41     }
    38     hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check
    42     hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check
    39     hg
    43     hg
    40   }
    44   }
    41 
    45 
    42   def setup_repository(source: String, root: Path, ssh: Option[SSH.Session] = None): Repository =
    46   def setup_repository(source: String, root: Path, ssh: Option[SSH.Session] = None): Repository =