--- a/src/Pure/Tools/build_process.scala Wed Mar 01 13:55:49 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Wed Mar 01 14:11:55 2023 +0100
@@ -29,8 +29,9 @@
case None => init(session, timeout = timeout)
case Some(db) =>
def ignore_error(msg: String) = {
- progress.echo_warning("Ignoring bad database " + db +
- " for session " + quote(session) + (if (msg == "") "" else ":\n" + msg))
+ progress.echo_warning(
+ "Ignoring bad database " + db + " for session " + quote(session) +
+ if_proper(msg, ":\n" + msg))
init(session, timeout = timeout)
}
try {