src/Pure/System/build.scala
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)))
       })
   }