use IsabelleText by default;
authorwenzelm
Mon, 07 Dec 2009 22:59:48 +0100
changeset 34753 dd8bdcb7dcba
parent 34752 e20ef5b33d17
child 34754 e8bb3052f3cb
use IsabelleText by default;
src/Tools/jEdit/dist-template/properties/jedit.props
--- 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