# HG changeset patch
# User wenzelm
# Date 1224618524 -7200
# Node ID 68e172602b867196db8261c9f159ad4bb49cccbd
# Parent  b353b4cd9bd430bc2182a3a52d5753cdb9f3e549
essential default properties for jEdit;

diff -r b353b4cd9bd4 -r 68e172602b86 src/Tools/jEdit/dist-template/properties/jedit.props
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Oct 21 21:48:44 2008 +0200
@@ -0,0 +1,23 @@
+#jEdit properties
+buffer.deepIndent=false
+buffer.encoding=UTF-8
+buffer.indentSize=2
+buffer.lineSeparator=\n
+buffer.maxLineLen=100
+buffer.noTabs=true
+buffer.tabSize=2
+fallbackEncodings=US-ASCII ISO-8859-15
+encodingDetectors=BOM XML-PI buffer-local-property
+delete-line.shortcut=A+d
+delete.shortcut2=C+d
+view.antiAlias=standard
+view.blockCaret=true
+view.caretBlink=false
+view.eolMarkers=false
+view.extendedState=0
+view.font=Lucida Sans Typewriter
+view.fontsize=18
+view.fracFontMetrics=true
+view.gutter.fontsize=12
+view.middleMousePaste=true
+view.showToolbar=false