# HG changeset patch
# User wenzelm
# Date 1420636746 -3600
# Node ID a1238edd8b3684cbab403870eb121bbe386a4c79
# Parent  2f4d64fba0d75bb66875b3c0e251b127fcd6f237
tuned;

diff -r 2f4d64fba0d7 -r a1238edd8b36 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Wed Jan 07 14:06:52 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Wed Jan 07 14:19:06 2015 +0100
@@ -269,13 +269,13 @@
         case ((graph, moved), i) =>
           val r = level(i)
           val d = r.deflection(graph, top_down)
-          val offset =
-            if (d < 0 && i > 0)
+          val dx =
+            if (d < 0.0 && i > 0)
               - (level(i - 1).distance(metrics, graph, r) min (- d))
-            else if (d >= 0 && i < level.length - 1)
+            else if (d >= 0.0 && i < level.length - 1)
               r.distance(metrics, graph, level(i + 1)) min d
             else d
-          (r.move(graph, offset), moved || d != 0)
+          (r.move(graph, dx), moved || d != 0.0)
       }
     }