clarified: follow "isabelle version -t";
authorwenzelm
Wed, 31 Mar 2021 23:13:13 +0200
changeset 73780 c52d819499a1
parent 73779 2cd23d587db9
child 73781 419edc7f3726
clarified: follow "isabelle version -t";
src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Wed Mar 31 22:58:17 2021 +0200
+++ b/src/Pure/General/mercurial.scala	Wed Mar 31 23:13:13 2021 +0200
@@ -132,7 +132,11 @@
 
     def id(rev: String = "tip"): String = identify(rev, options = "-i")
 
-    def tags(rev: String = "tip"): String = identify(rev, options = "-t")
+    def tags(rev: String = "tip"): String =
+    {
+      val result = identify(rev, options = "-t")
+      Library.space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
+    }
 
     def paths(args: String = "", options: String = ""): List[String] =
       hg.command("paths", args = args, options = options).check.out_lines