# HG changeset patch
# User wenzelm
# Date 1730575661 -3600
# Node ID 301feaa854062e98706987a065c30bd023916974
# Parent  f0fccb521124d99aa9abc8e249ca5020633d7355
tuned;

diff -r f0fccb521124 -r 301feaa85406 src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala	Sat Nov 02 20:24:53 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Sat Nov 02 20:27:41 2024 +0100
@@ -78,8 +78,9 @@
   })
   tree.addMouseListener(new MouseAdapter {
     override def mousePressed(e: MouseEvent): Unit =
-      if (e.getClickCount == 2)
+      if (e.getClickCount == 2) {
         point_action(tree.getPathForLocation(e.getX, e.getY))
+      }
   })
 
   private val tree_pane = new ScrollPane(Component.wrap(tree))