# HG changeset patch
# User wenzelm
# Date 1389034783 -3600
# Node ID b411e99d1581662149fb3ef343dd75b04cf5f4a5
# Parent  8cccfb8f1d366dea5ffefd449ec69c84e44c1d92
more informative error message;

diff -r 8cccfb8f1d36 -r b411e99d1581 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Jan 06 19:47:11 2014 +0100
+++ b/src/Pure/Tools/build.scala	Mon Jan 06 19:59:43 2014 +0100
@@ -117,7 +117,8 @@
         (Graph.string[Session_Info] /: infos) {
           case (graph, (name, info)) =>
             if (graph.defined(name))
-              error("Duplicate session " + quote(name) + Position.here(info.pos))
+              error("Duplicate session " + quote(name) + Position.here(info.pos) +
+                Position.here(graph.get_node(name).pos))
             else graph.new_node(name, info)
         }
       val graph2 =