src/Tools/jEdit/etc/settings
changeset 55432 9c53198dbb1c
parent 54324 dabaf9ca1513
child 56422 7490555d7dff