src/Pure/General/mercurial.scala
changeset 64027 4a33d740c9dc
parent 64020 355b78441650
child 64028 6cc79f1c82cd
equal deleted inserted replaced
64026:cbecd26e063f 64027:4a33d740c9dc
    43       command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse ""
    43       command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse ""
    44 
    44 
    45     def manifest(rev: String = "", options: String = ""): List[String] =
    45     def manifest(rev: String = "", options: String = ""): List[String] =
    46       command("manifest " + options + opt_rev(rev)).check.out_lines
    46       command("manifest " + options + opt_rev(rev)).check.out_lines
    47 
    47 
       
    48     def log(rev: String = "", options: String = ""): String =
       
    49       Library.trim_line(command("log " + options + opt_rev(rev)).check.out)
       
    50 
    48     def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
    51     def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
    49       command("pull " + options + opt_rev(rev) + optional(remote)).check
    52       command("pull " + options + opt_rev(rev) + optional(remote)).check
    50 
    53 
    51     def update(rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
    54     def update(rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
    52     {
    55     {