# HG changeset patch
# User wenzelm
# Date 1475842640 -7200
# Node ID fef1a0a59c126c7aa11238652e29008c4e57c24f
# Parent  d57c7295f60184d4a0726c589eabf4c2cedea1f3
more operations;

diff -r d57c7295f601 -r fef1a0a59c12 src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Fri Oct 07 13:58:10 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 14:17:20 2016 +0200
@@ -51,6 +51,16 @@
 
   object Log_File
   {
+    def apply(path: Path): Log_File =
+    {
+      val (path_name, ext) = path.expand.split_ext
+      val text =
+        if (ext == "gz") File.read_gzip(path)
+        else if (ext == "xz") File.read_xz(path)
+        else File.read(path)
+      apply(path_name.base.implode, text)
+    }
+
     def apply(name: String, lines: List[String]): Log_File =
       new Log_File(name, lines)