tuned;

--- 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))