diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/General/mercurial.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -100,7 +100,7 @@
 
   sealed case class Archive_Info(lines: List[String]) {
     def id: Option[String] = lines.collectFirst({ case Archive_Node(a) => a })
-    def tags: List[String] = for (Archive_Tag(tag) <- lines if tag != "tip") yield tag
+    def tags: List[String] = for (case Archive_Tag(tag) <- lines if tag != "tip") yield tag
   }
 
   def archive_info(root: Path): Option[Archive_Info] = {