changeset 57908 | 1937603dbdf2 |
parent 57867 | abae8aff6262 |
child 57979 | fc136831d6ca |
--- a/src/Tools/jEdit/src/plugin.scala Tue Aug 12 00:23:30 2014 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 12 12:06:22 2014 +0200 @@ -373,7 +373,7 @@ PIDE.plugin = this Isabelle_System.init() - Isabelle_Font.install_fonts() + GUI.install_fonts() PIDE.options.update(Options.init()) PIDE.completion_history.load()