--- /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