changeset 75906 | 2167b9e3157a |
parent 75776 | 72e77c8307ec |
child 75968 | 5a782ca6872b |
--- a/src/Pure/Admin/build_log.scala Fri Aug 19 16:19:59 2022 +0200 +++ b/src/Pure/Admin/build_log.scala Fri Aug 19 16:46:00 2022 +0200 @@ -108,8 +108,8 @@ def apply(file: JFile): Log_File = { val name = file.getName val text = - if (name.endsWith(".gz")) File.read_gzip(file) - else if (name.endsWith(".xz")) File.read_xz(file) + if (File.is_gz(name)) File.read_gzip(file) + else if (File.is_xz(name)) File.read_xz(file) else File.read(file) apply(name, text) }