| 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