src/Tools/jEdit/etc/settings
changeset 57978 8f4a332500e4
parent 56835 f05dadddf095
child 58641 5697ae9a683a