changeset 65365 | d32e702d7ab8 |
parent 65360 | 3ff88fece1f6 |
child 65372 | b722ee40c26c |
--- 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 {