src/Tools/jEdit/dist-template/properties/jedit.props
changeset 34623 a356a8ee6f00
parent 34619 e89b6ec97910
child 34626 7124433be8be
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Fri Jun 26 18:23:30 2009 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Fri Jun 26 18:24:03 2009 +0200
@@ -1,6 +1,6 @@
 #jEdit properties
 buffer.deepIndent=false
-buffer.encoding=UTF-8-isabelle
+buffer.encoding=UTF-8-Isabelle
 buffer.indentSize=2
 buffer.lineSeparator=\n
 buffer.maxLineLen=100