# HG changeset patch
# User wenzelm
# Date 1617225193 -7200
# Node ID c52d819499a1ec7db9937a99b0f9b3139b2f69ef
# Parent  2cd23d587db90f44d55514121a99ea716b104bff
clarified: follow "isabelle version -t";

diff -r 2cd23d587db9 -r c52d819499a1 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