src/Tools/jEdit/etc/settings
changeset 47619 0d3e95375bb7
parent 47235 a92d3620e156
child 49612 e6a53d203362