author | wenzelm |
Mon, 07 Dec 2009 22:59:48 +0100 | |
changeset 34753 | dd8bdcb7dcba |
parent 34752 | e20ef5b33d17 |
child 34754 | e8bb3052f3cb |
src/Tools/jEdit/dist-template/properties/jedit.props | file | annotate | diff | comparison | revisions |
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Mon Dec 07 22:41:32 2009 +0100 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Mon Dec 07 22:59:48 2009 +0100 @@ -184,7 +184,7 @@ view.caretBlink=false view.eolMarkers=false view.extendedState=0 -view.font=Lucida Sans Typewriter +view.font=IsabelleText view.fontsize=18 view.fracFontMetrics=false view.gutter.fontsize=12