src/Pure/Admin/build_log.scala
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)
     }