changeset 50465 | 0afb01666df2 |
parent 49954 | 44658062d822 |
child 50468 | 7a2a4b84c5ee |
--- a/src/Tools/Graphview/src/graph_panel.scala Mon Dec 10 17:44:17 2012 +0100 +++ b/src/Tools/Graphview/src/graph_panel.scala Mon Dec 10 19:17:16 2012 +0100 @@ -47,7 +47,7 @@ private val gfx_aux = new BufferedImage(1, 1, BufferedImage.TYPE_INT_RGB).createGraphics - gfx_aux.setFont(visualizer.Font()) + gfx_aux.setFont(visualizer.font) gfx_aux.setRenderingHints(visualizer.rendering_hints) def node(at: Point2D): Option[String] =