src/Tools/Graphview/src/graph_panel.scala
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] =