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