tuned message;
authorwenzelm
Sun, 07 Aug 2022 23:06:29 +0200
changeset 75793 5e00c5ffc040
parent 75792 4e273b4e04e8
child 75794 1c3c31319974
tuned message;
src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Aug 07 20:36:01 2022 +0200
+++ b/src/Pure/Tools/build.scala	Sun Aug 07 23:06:29 2022 +0200
@@ -39,7 +39,8 @@
         case None => no_timings
         case Some(db) =>
           def ignore_error(msg: String) = {
-            progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
+            progress.echo_warning("Ignoring bad database " + db +
+              " for session " + quote(session_name) + (if (msg == "") "" else ":\n" + msg))
             no_timings
           }
           try {