src/Tools/jEdit/dist-template/properties/jedit.props
changeset 34623 a356a8ee6f00
parent 34619 e89b6ec97910
child 34626 7124433be8be
equal deleted inserted replaced
34622:b1b88879c515 34623:a356a8ee6f00
     1 #jEdit properties
     1 #jEdit properties
     2 buffer.deepIndent=false
     2 buffer.deepIndent=false
     3 buffer.encoding=UTF-8-isabelle
     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