changeset 72885 | 1b0f81e556a2 |
parent 72860 | 64378eaf393d |
child 73024 | 337e1b135d2f |
--- a/src/Pure/Admin/build_log.scala Fri Dec 11 17:58:01 2020 +0100 +++ b/src/Pure/Admin/build_log.scala Sat Dec 12 12:45:21 2020 +0100 @@ -656,7 +656,7 @@ } def uncompress_errors(bytes: Bytes, cache: XZ.Cache = XZ.cache()): List[String] = - if (bytes.isEmpty) Nil + if (bytes.is_empty) Nil else { XML.Decode.list(YXML.string_of_body)(YXML.parse_body(bytes.uncompress(cache = cache).text)) }