src/Pure/Tools/build.scala
changeset 65365 d32e702d7ab8
parent 65360 3ff88fece1f6
child 65372 b722ee40c26c
     1.1 --- a/src/Pure/Tools/build.scala	Mon Apr 03 23:12:44 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Apr 03 23:31:31 2017 +0200
     1.3 @@ -43,7 +43,8 @@
     1.4          case Some(database) =>
     1.5            def ignore_error(msg: String) =
     1.6            {
     1.7 -            Output.warning("Ignoring bad database: " + database + (if (msg == "") "" else "\n" + msg))
     1.8 +            Output.warning("Ignoring bad database: " +
     1.9 +              database.expand + (if (msg == "") "" else "\n" + msg))
    1.10              no_timings
    1.11            }
    1.12            try {