src/Tools/jEdit/etc/options
changeset 82909 e4fae2227594
parent 82628 49e4ce0c6aa1