src/Tools/jEdit/etc/options
changeset 64443 857acb970dfa
parent 63474 f66e3c3b0fb1
child 64835 fd1efd6dd385