tuned properties;
authorwenzelm
Tue Sep 07 23:53:27 2010 +0200 (2010-09-07)
changeset 39180e1d160a9bd5f
parent 39179 591bbab9ef59
child 39181 2257eded8323
tuned properties;
src/Tools/jEdit/dist-template/properties/jedit.props
     1.1 --- a/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Sep 07 23:23:19 2010 +0200
     1.2 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Sep 07 23:53:27 2010 +0200
     1.3 @@ -177,6 +177,7 @@
     1.4  end.shortcut=
     1.5  fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
     1.6  firstTime=false
     1.7 +foldPainter=Circle
     1.8  home.shortcut=
     1.9  insert-newline-indent.shortcut=
    1.10  insert-newline.shortcut=ENTER