--- a/src/Pure/General/path.scala Mon May 10 20:09:47 2021 +0200
+++ b/src/Pure/General/path.scala Mon May 10 22:18:12 2021 +0200
@@ -213,6 +213,7 @@
}
def xz: Path = ext("xz")
+ def xml: Path = ext("xml")
def html: Path = ext("html")
def tex: Path = ext("tex")
def pdf: Path = ext("pdf")