author | wenzelm |
Tue, 27 Jan 2009 22:13:56 +0100 | |
changeset 34506 | bc22e49358f8 |
parent 34505 | 87f4f70d61bb |
child 34507 | 018bad916757 |
--- a/src/Tools/jEdit/src/jedit/OptionPane.scala Tue Jan 27 19:52:56 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/OptionPane.scala Tue Jan 27 22:13:56 2009 +0100 @@ -44,7 +44,7 @@ addComponent(Isabelle.Property("font-size.title"), { try { if (Isabelle.Property("font-size") != null) - fontSize.setValue(Integer.valueOf(Isabelle.Property("font-size"))) + fontSize.setValue(Isabelle.Property("font-size").toInt) } catch { case e : NumberFormatException =>