src/Tools/jEdit/dist-template/properties/jedit.props
changeset 34619 e89b6ec97910
parent 34613 71fb6ab6ec57
child 34623 a356a8ee6f00
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Thu Jun 25 21:15:28 2009 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Thu Jun 25 23:03:09 2009 +0200
@@ -1,12 +1,12 @@
 #jEdit properties
 buffer.deepIndent=false
-buffer.encoding=UTF-8
+buffer.encoding=UTF-8-isabelle
 buffer.indentSize=2
 buffer.lineSeparator=\n
 buffer.maxLineLen=100
 buffer.noTabs=true
 buffer.tabSize=2
-fallbackEncodings=US-ASCII ISO-8859-15
+fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
 firstTime=false
 tip.show=false
 encodingDetectors=BOM XML-PI buffer-local-property