tuned;
authorwenzelm
Wed, 01 Mar 2023 14:11:55 +0100
changeset 77441 7751922c6668
parent 77440 80f7a7b66224
child 77442 9969b6aed223
tuned;
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 {