src/Tools/jEdit/etc/settings
changeset 48401 e740216ca28d
parent 47235 a92d3620e156
child 49612 e6a53d203362