equal
deleted
inserted
replaced
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 = |