changeset 48370 | d0fa3efec93b |
parent 48368 | dc538eef2cf2 |
child 48373 | 527e2bad7cca |
--- a/src/Pure/System/build.scala Fri Jul 20 17:43:55 2012 +0200 +++ b/src/Pure/System/build.scala Fri Jul 20 18:50:33 2012 +0200 @@ -192,7 +192,7 @@ catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session entry " + - quote(entry.name) + " (file " + quote(root.toString) + ")") + quote(entry.name) + Position.str_of(Position.file(root))) }) }