src/Pure/General/mercurial.scala
changeset 77218 86217697863c
parent 76883 186e07be32c3
child 77368 7c57d9586f4c
--- a/src/Pure/General/mercurial.scala	Mon Feb 06 16:26:40 2023 +0100
+++ b/src/Pure/General/mercurial.scala	Mon Feb 06 16:29:19 2023 +0100
@@ -248,7 +248,7 @@
 
     def tags(rev: String = "tip"): String = {
       val result = identify(rev, options = "-t")
-      Library.space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
+      space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
     }
 
     def paths(args: String = "", options: String = ""): List[String] =