src/Tools/Graphview/graph_panel.scala
changeset 59294 126293918a37
parent 59291 506660c6792f
child 59302 4d985afc0565
--- a/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 23:05:17 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 23:29:38 2015 +0100
@@ -96,7 +96,7 @@
       gfx.fillRect(0, 0, peer.getWidth, peer.getHeight)
       gfx.transform(Transform())
 
-      visualizer.Drawer.paint_all_visible(gfx, true)
+      visualizer.paint_all_visible(gfx)
     }
   }
   private val paint_panel = new Paint_Panel