src/Tools/jEdit/etc/settings
changeset 51098 22d5c010ef5c
parent 50746 429075aeb618
child 53489 97222a86aec0