use IsabelleText by default;
authorwenzelm
Mon Dec 07 22:59:48 2009 +0100 (2009-12-07)
changeset 34753dd8bdcb7dcba
parent 34752 e20ef5b33d17
child 34754 e8bb3052f3cb
use IsabelleText by default;
src/Tools/jEdit/dist-template/properties/jedit.props
     1.1 --- a/src/Tools/jEdit/dist-template/properties/jedit.props	Mon Dec 07 22:41:32 2009 +0100
     1.2 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Mon Dec 07 22:59:48 2009 +0100
     1.3 @@ -184,7 +184,7 @@
     1.4  view.caretBlink=false
     1.5  view.eolMarkers=false
     1.6  view.extendedState=0
     1.7 -view.font=Lucida Sans Typewriter
     1.8 +view.font=IsabelleText
     1.9  view.fontsize=18
    1.10  view.fracFontMetrics=false
    1.11  view.gutter.fontsize=12