--- a/src/Tools/Graphview/graphview.scala Wed Jan 28 19:15:13 2015 +0100
+++ b/src/Tools/Graphview/graphview.scala Wed Jan 28 19:18:08 2015 +0100
@@ -135,7 +135,7 @@
}
}
- def paint_all_visible(gfx: Graphics2D)
+ def paint(gfx: Graphics2D)
{
gfx.setRenderingHints(Metrics.rendering_hints)