author | wenzelm |
Sun, 07 Aug 2022 23:06:29 +0200 | |
changeset 75793 | 5e00c5ffc040 |
parent 75792 | 4e273b4e04e8 |
child 75794 | 1c3c31319974 |
--- 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 {