# HG changeset patch
# User wenzelm
# Date 1475523370 -7200
# Node ID 4a33d740c9dc9e77d9a628a41ffb9df003f965cf
# Parent  cbecd26e063f49849c6cd495bf76a00bc2b23e1a
proper log output;

diff -r cbecd26e063f -r 4a33d740c9dc src/Pure/General/mercurial.scala
--- 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
 
diff -r cbecd26e063f -r 4a33d740c9dc src/Pure/Tools/build_history.scala
--- a/src/Pure/Tools/build_history.scala	Mon Oct 03 21:14:21 2016 +0200
+++ b/src/Pure/Tools/build_history.scala	Mon Oct 03 21:36:10 2016 +0200
@@ -29,7 +29,7 @@
     build_args: List[String] = Nil): Process_Result =
   {
     hg.update(rev = rev, clean = true)
-    if (verbose) hg.command("log -l1").check.print
+    if (verbose) Output.writeln(hg.log(rev, options = "-l1"))
 
     def bash(script: String): Process_Result =
       Isabelle_System.bash("env ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) +