author | wenzelm |
Mon, 03 Apr 2017 23:31:31 +0200 | |
changeset 65365 | d32e702d7ab8 |
parent 65364 | db7c97cdcfe7 |
child 65366 | 10ca63a18e56 |
child 65397 | 9cdafcfb28bf |
--- 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 {