# HG changeset patch
# User wenzelm
# Date 1420558997 -3600
# Node ID 848e27e4ac37ee9219e6740d022ab8c521260f79
# Parent  15cd9bcd6ddbf5e488f7379113c7d7bb5d559398
proper translate vertex (cf. 4d985afc0565);

diff -r 15cd9bcd6ddb -r 848e27e4ac37 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Tue Jan 06 16:41:31 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Tue Jan 06 16:43:17 2015 +0100
@@ -324,7 +324,7 @@
   {
     if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this
     else {
-      val output_graph1 = output_graph.map_node(v, p => Layout.Point(p.x + dy, p.y + dy))
+      val output_graph1 = output_graph.map_node(v, p => Layout.Point(p.x + dx, p.y + dy))
       new Layout(metrics, input_graph, output_graph1)
     }
   }