src/Tools/jEdit/etc/settings
changeset 51750 cb154917a496
parent 50746 429075aeb618
child 53489 97222a86aec0