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] =