src/Tools/jEdit/src/graphview_dockable.scala
changeset 59290 569a8109eeb2
parent 59288 b1086f3e4590
child 59392 02bacfc31446
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 05 21:44:05 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 05 21:47:12 2015 +0100
@@ -78,7 +78,7 @@
           override def selection_color = view.getTextArea.getPainter.getSelectionColor
           override def error_color = PIDE.options.color_value("error_color")
 
-          override def font() =
+          override def make_font(): Font =
             GUI.imitate_font(Font_Info.main().font,
               PIDE.options.string("graphview_font_family"),
               PIDE.options.real("graphview_font_scale"))