# HG changeset patch
# User wenzelm
# Date 1421617598 -3600
# Node ID db65d45b6740ff11755f05af1f8d873651577968
# Parent  4de91de47a6cee91dafa2ce61bf6a1ccbdb962ee
suppress some controls that don't work yet;

diff -r 4de91de47a6c -r db65d45b6740 src/Tools/Graphview/graph_panel.scala
--- 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 {