src/Tools/jEdit/etc/settings
changeset 71751 abf3e80bd815
parent 70220 089753519be0
child 71790 97fc4f657bda