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