| changeset 80350 | 96843eb96493 |
| parent 80303 | 11fee9e6ba43 |
| child 80447 | 325907d85977 |
--- a/src/Pure/Build/export.scala Tue Jun 11 11:07:48 2024 +0200 +++ b/src/Pure/Build/export.scala Tue Jun 11 14:18:19 2024 +0200 @@ -194,7 +194,7 @@ def text: String = bytes.text - def yxml: XML.Body = YXML.parse_body(UTF8.decode_permissive(bytes), cache = cache) + def yxml: XML.Body = YXML.parse_body(bytes.text, cache = cache) } def make_regex(pattern: String): Regex = {