# HG changeset patch
# User wenzelm
# Date 1680117374 -7200
# Node ID a8c52c99fa92999e4950157a300e43592960a32f
# Parent  4649c7bfd3f0402049e50e6fc149a8354b61ffbe
tuned messages;

diff -r 4649c7bfd3f0 -r a8c52c99fa92 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed Mar 29 20:56:43 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed Mar 29 21:16:14 2023 +0200
@@ -186,7 +186,7 @@
     def text: String = cat_lines(lines)
 
     def err(msg: String): Nothing =
-      error("Error in log file " + quote(name) + ": " + msg)
+      error("Bad log file " + quote(name) + ": " + msg)
 
 
     /* date format */
@@ -1181,8 +1181,11 @@
       }
       else {
         error(cat_lines(List.from(
-          for ((name, rev_errs) <- errors.iterator_list)
-            yield "Error(s) in log file " + quote(name) + ":\n" + cat_lines(rev_errs.reverse))))
+          for ((name, rev_errs) <- errors.iterator_list) yield {
+            val err = "The error(s) above occurred in " + quote(name)
+            cat_lines((err :: rev_errs).reverse)
+          }
+        )))
       }
     }
   }