--- a/src/Tools/Graphview/graph_panel.scala Sun Jan 18 22:43:53 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Sun Jan 18 22:46:38 2015 +0100
@@ -237,8 +237,11 @@
if (clicks < 2) {
if (right_click) {
- val menu = Popups(panel, visualizer.find_node(c), visualizer.Selection.get())
- menu.show(panel.peer, at.x, at.y)
+ // FIXME
+ if (false) {
+ val menu = Popups(panel, visualizer.find_node(c), visualizer.Selection.get())
+ menu.show(panel.peer, at.x, at.y)
+ }
}
else {
(visualizer.find_node(c), m) match {