# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1720516275 -7200
# Node ID c54a4c2db5b7d419423213e0dd254b612046b4c1
# Parent  ae881e1480bbd104e286cc212808c20ade7e7dc4
tuned;

diff -r ae881e1480bb -r c54a4c2db5b7 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Jul 09 11:23:50 2024 +0100
+++ b/src/Pure/Build/build_manager.scala	Tue Jul 09 11:11:15 2024 +0200
@@ -604,6 +604,7 @@
 
   case class Report(kind: String, id: Long, dir: Path) {
     private val log_name = "build-manager"
+    private val diff_ext = "diff"
 
     private def log_file = dir + Path.basic(log_name).log
     private def log_file_gz = dir + Path.basic(log_name).log.gz
@@ -614,20 +615,21 @@
 
     def progress: Progress = new File_Progress(log_file)
 
+    private def read_gz(file: Path, ext: String): Option[(String, String)] =
+      if (!File.is_gz(file.file_name) || file.drop_ext.get_ext != ext) None
+      else Some(file.drop_ext.drop_ext.file_name -> File.read_gzip(file))
+
     def read: Report.Data = {
       val log =
         if_proper(ok, if (log_file.is_file) File.read(log_file) else File.read_gzip(log_file_gz))
-      val diffs =
-        for {
-          name <- File.read_dir(dir)
-          file = dir + Path.basic(name)
-          if file.get_ext == "gz" && file.drop_ext.get_ext == "diff"
-        } yield file.drop_ext.drop_ext.file_name -> File.read_gzip(file)
+
+      val diffs = File.read_dir(dir).flatMap(name => read_gz(dir + Path.basic(name), diff_ext))
+
       Report.Data(log, diffs)
     }
 
     def write_diff(name: String, diff: String): Unit =
-      if (diff.nonEmpty) File.write_gzip(dir + Path.basic(name + ".diff").gz, diff)
+      if (diff.nonEmpty) File.write_gzip(dir + Path.basic(name).ext(diff_ext).gz, diff)
 
     def result(uuid: Option[UUID.T]): Result = {
       val End = """^Job ended at [^,]+, with status (\w+)$""".r