author | wenzelm |
Wed, 28 Nov 2018 13:59:29 +0100 | |
changeset 69359 | 3b709d9074ec |
parent 69358 | 71ef6e6da3dc |
child 69360 | dc9a39c3f75d |
--- a/src/Tools/jEdit/src/graphview_dockable.scala Wed Nov 28 12:05:50 2018 +0100 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Wed Nov 28 13:59:29 2018 +0100 @@ -78,7 +78,7 @@ } override def make_font(): Font = - if (editor_style) Font_Info.main(PIDE.options.real("graphview_font_scale")).font + if (editor_style) GUI.imitate_font(Font_Info.main().font) else GUI.imitate_font(Font_Info.main().font, family = options.string("graphview_font_family"),