src/Tools/jEdit/src/jEdit.props
changeset 63757 a9159d30070f
parent 63749 4fe8cfaeb1fc
child 63760 b1088b1e3b7e
equal deleted inserted replaced
63754:23b013b6b2fb 63757:a9159d30070f
   175 encoding.opt-out.x-windows-50221=true
   175 encoding.opt-out.x-windows-50221=true
   176 encoding.opt-out.x-windows-iso2022jp=true
   176 encoding.opt-out.x-windows-iso2022jp=true
   177 encodingDetectors=BOM XML-PI buffer-local-property
   177 encodingDetectors=BOM XML-PI buffer-local-property
   178 end.shortcut=
   178 end.shortcut=
   179 expand-abbrev.shortcut2=CA+SPACE
   179 expand-abbrev.shortcut2=CA+SPACE
       
   180 expand-folds.shortcut=
   180 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
   181 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
   181 firstTime=false
   182 firstTime=false
   182 focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
   183 focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
   183 foldPainter=Circle
   184 foldPainter=Circle
   184 gatchan.highlight.overview=false
   185 gatchan.highlight.overview=false