# HG changeset patch
# User wenzelm
# Date 1260223188 -3600
# Node ID dd8bdcb7dcbaa3b4ad53fd4e1343750a6be10698
# Parent  e20ef5b33d17114fd2581c389312854f4e8f1873
use IsabelleText by default;

diff -r e20ef5b33d17 -r dd8bdcb7dcba 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