install_fonts;
authorwenzelm
Thu, 10 Dec 2009 13:47:50 +0100
changeset 347771fa466333361
parent 34776 bb5d68f7fd5e
child 34778 49245d68f7e4
install_fonts;
src/Tools/jEdit/src/jedit/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 23:45:42 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Dec 10 13:47:50 2009 +0100
     1.3 @@ -145,7 +145,7 @@
     1.4    {
     1.5      Isabelle.plugin = this
     1.6      Isabelle.system = new Isabelle_System
     1.7 -    Isabelle.system.register_fonts()
     1.8 +    Isabelle.system.install_fonts()
     1.9    }
    1.10  
    1.11    override def stop()