src/Tools/jEdit/etc/settings
changeset 55791 5821b1937fa5
parent 54324 dabaf9ca1513
child 56422 7490555d7dff