src/Pure/General/mercurial.scala
changeset 71601 97ccf48c2f0c
parent 71562 794c8b0ad8f1
child 71684 5036edb025b7
equal deleted inserted replaced
71600:64aad1e46f98 71601:97ccf48c2f0c
    42     hg
    42     hg
    43   }
    43   }
    44 
    44 
    45   def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] =
    45   def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] =
    46   {
    46   {
    47     def find(root: Path): Option[Repository] =
    47     @tailrec def find(root: Path): Option[Repository] =
    48       if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
    48       if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
    49       else if (root.is_root) None
    49       else if (root.is_root) None
    50       else find(root + Path.parent)
    50       else find(root + Path.parent)
    51 
    51 
    52     find(ssh.expand_path(start))
    52     find(ssh.expand_path(start))
    93           " --noninteractive " + name + " " + options + " " + args
    93           " --noninteractive " + name + " " + options + " " + args
    94       ssh.execute(cmdline)
    94       ssh.execute(cmdline)
    95     }
    95     }
    96 
    96 
    97     def add(files: List[Path]): Unit =
    97     def add(files: List[Path]): Unit =
    98       hg.command("add", files.map(ssh.bash_path(_)).mkString(" "))
    98       hg.command("add", files.map(ssh.bash_path).mkString(" "))
    99 
    99 
   100     def archive(target: String, rev: String = "", options: String = ""): Unit =
   100     def archive(target: String, rev: String = "", options: String = ""): Unit =
   101       hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
   101       hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
   102 
   102 
   103     def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
   103     def heads(template: String = "{node|short}\n", options: String = ""): List[String] =