# HG changeset patch # User wenzelm # Date 1260449270 -3600 # Node ID 1fa46633336104424e8c42eb422a9ae842e0adaf # Parent bb5d68f7fd5e7a810cb550fed750150a13fe8455 install_fonts; diff -r bb5d68f7fd5e -r 1fa466333361 src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Tue Dec 08 23:45:42 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Thu Dec 10 13:47:50 2009 +0100 @@ -145,7 +145,7 @@ { Isabelle.plugin = this Isabelle.system = new Isabelle_System - Isabelle.system.register_fonts() + Isabelle.system.install_fonts() } override def stop()