# HG changeset patch
# User wenzelm
# Date 1614633993 -3600
# Node ID 2dd1fd9112d94837ac0d4e586948c0c60ff56104
# Parent  0ffcad1f61305dec6c7416a4418a5449a58046ac
tuned --- silence odd warning;

diff -r 0ffcad1f6130 -r 2dd1fd9112d9 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Mon Mar 01 22:22:12 2021 +0100
+++ b/src/Tools/Graphview/layout.scala	Mon Mar 01 22:26:33 2021 +0100
@@ -294,10 +294,12 @@
           val r = level(i)
           val d = r.deflection(graph, top_down)
           val dx =
-            if (d < 0.0 && i > 0)
+            if (d < 0.0 && i > 0) {
               - (level(i - 1).distance(metrics, graph, r) min (- d))
-            else if (d >= 0.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, dx), moved || d != 0.0)
       }