src/Pure/General/mercurial.scala
changeset 64027 4a33d740c9dc
parent 64020 355b78441650
child 64028 6cc79f1c82cd
--- a/src/Pure/General/mercurial.scala	Mon Oct 03 21:14:21 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Mon Oct 03 21:36:10 2016 +0200
@@ -45,6 +45,9 @@
     def manifest(rev: String = "", options: String = ""): List[String] =
       command("manifest " + options + opt_rev(rev)).check.out_lines
 
+    def log(rev: String = "", options: String = ""): String =
+      Library.trim_line(command("log " + options + opt_rev(rev)).check.out)
+
     def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
       command("pull " + options + opt_rev(rev) + optional(remote)).check