# HG changeset patch
# User wenzelm
# Date 1677676315 -3600
# Node ID 7751922c66683ef7d752d17017ad864012d1f263
# Parent  80f7a7b66224b5b6cd39c1c6dd2660cc992b939e
tuned;

diff -r 80f7a7b66224 -r 7751922c6668 src/Pure/Tools/build_process.scala
--- 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 {