src/Pure/General/mercurial.scala
changeset 65818 94cad7590015
parent 65559 7ff7781913a4
child 65819 ff3dc9325eaa
equal deleted inserted replaced
65814:3039d4aa7143 65818:94cad7590015
    66       ssh match {
    66       ssh match {
    67         case None => root.is_dir
    67         case None => root.is_dir
    68         case Some(ssh) => ssh.is_dir(root)
    68         case Some(ssh) => ssh.is_dir(root)
    69       }
    69       }
    70     if (present) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
    70     if (present) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
    71     else clone_repository(source, root, options = "--noupdate", ssh = ssh)
    71     else clone_repository(source, root, options = "--pull --noupdate", ssh = ssh)
    72   }
    72   }
    73 
    73 
    74   class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session])
    74   class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session])
    75   {
    75   {
    76     hg =>
    76     hg =>