tuned message;
authorwenzelm
Mon, 03 Apr 2017 23:31:31 +0200
changeset 65365 d32e702d7ab8
parent 65364 db7c97cdcfe7
child 65366 10ca63a18e56
child 65397 9cdafcfb28bf
tuned message;
src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Apr 03 23:12:44 2017 +0200
+++ b/src/Pure/Tools/build.scala	Mon Apr 03 23:31:31 2017 +0200
@@ -43,7 +43,8 @@
         case Some(database) =>
           def ignore_error(msg: String) =
           {
-            Output.warning("Ignoring bad database: " + database + (if (msg == "") "" else "\n" + msg))
+            Output.warning("Ignoring bad database: " +
+              database.expand + (if (msg == "") "" else "\n" + msg))
             no_timings
           }
           try {