src/Pure/Build/export.scala
changeset 80480 972f7a4cdc0e
parent 80447 325907d85977
--- a/src/Pure/Build/export.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/Build/export.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -195,7 +195,7 @@
     def text: String = bytes.text
 
     def yxml(recode: String => String = identity): XML.Body =
-      YXML.parse_body(bytes.text, recode = recode, cache = cache)
+      YXML.parse_body(bytes, recode = recode, cache = cache)
   }
 
   def make_regex(pattern: String): Regex = {