# HG changeset patch
# User wenzelm
# Date 1491255091 -7200
# Node ID d32e702d7ab8e850f9668b0ad8ea77f9859913ec
# Parent  db7c97cdcfe7ffa59bb370f5f576e45dacbc0210
tuned message;

diff -r db7c97cdcfe7 -r d32e702d7ab8 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 {