tuned log: omit previous changeset;
authorFabian Huch <huch@in.tum.de>
Wed, 10 Jul 2024 09:58:32 +0200
changeset 80541 5ebfe18e3952
parent 80540 f86bcf439837
child 80542 dd86d35375a7
tuned log: omit previous changeset;
src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Wed Jul 10 08:37:54 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Wed Jul 10 09:58:32 2024 +0200
@@ -810,10 +810,11 @@
       }
 
     private def log(repository: Mercurial.Repository, rev0: String, rev: String): String =
-      if (rev0.isEmpty || rev.isEmpty) ""
+      if (rev0.isEmpty || rev.isEmpty || rev0 == rev) ""
       else {
         val log_opts = "--graph --color always"
-        val cmd = repository.command_line("log", Mercurial.opt_rev(rev0 + ":" + rev), log_opts)
+        val rev1 = "children(" + rev0 + ")"
+        val cmd = repository.command_line("log", Mercurial.opt_rev(rev1 + ":" + rev), log_opts)
         Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out
       }