src/Tools/jEdit/dist-template/properties/jedit.props
changeset 34619 e89b6ec97910
parent 34613 71fb6ab6ec57
child 34623 a356a8ee6f00
equal deleted inserted replaced
34618:e45052ff7233 34619:e89b6ec97910
     1 #jEdit properties
     1 #jEdit properties
     2 buffer.deepIndent=false
     2 buffer.deepIndent=false
     3 buffer.encoding=UTF-8
     3 buffer.encoding=UTF-8-isabelle
     4 buffer.indentSize=2
     4 buffer.indentSize=2
     5 buffer.lineSeparator=\n
     5 buffer.lineSeparator=\n
     6 buffer.maxLineLen=100
     6 buffer.maxLineLen=100
     7 buffer.noTabs=true
     7 buffer.noTabs=true
     8 buffer.tabSize=2
     8 buffer.tabSize=2
     9 fallbackEncodings=US-ASCII ISO-8859-15
     9 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
    10 firstTime=false
    10 firstTime=false
    11 tip.show=false
    11 tip.show=false
    12 encodingDetectors=BOM XML-PI buffer-local-property
    12 encodingDetectors=BOM XML-PI buffer-local-property
    13 delete-line.shortcut=A+d
    13 delete-line.shortcut=A+d
    14 delete.shortcut2=C+d
    14 delete.shortcut2=C+d