src/Tools/jEdit/etc/options
changeset 81474 a3dc66165d15
parent 77612 3e235fab64db
child 82547 cbeef60a8435