src/Pure/General/mercurial.scala
changeset 64033 2989c1f2593a
parent 64028 6cc79f1c82cd
child 64138 cf0c8c5782af
equal deleted inserted replaced
64032:46c1ffc78d73 64033:2989c1f2593a
    44       command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse ""
    44       command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse ""
    45 
    45 
    46     def manifest(rev: String = "", options: String = ""): List[String] =
    46     def manifest(rev: String = "", options: String = ""): List[String] =
    47       command("manifest " + options + opt_rev(rev)).check.out_lines
    47       command("manifest " + options + opt_rev(rev)).check.out_lines
    48 
    48 
    49     def log(rev: String = "", options: String = ""): String =
    49     def log(rev: String = "", template: String = "", options: String = ""): String =
    50       Library.trim_line(command("log " + options + opt_rev(rev)).check.out)
    50       Library.trim_line(command("log " + options + opt_rev(rev) + opt_template(template)).check.out)
    51 
    51 
    52     def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
    52     def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
    53       command("pull " + options + opt_rev(rev) + optional(remote)).check
    53       command("pull " + options + opt_rev(rev) + optional(remote)).check
    54 
    54 
    55     def update(rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
    55     def update(rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")