src/Tools/jEdit/etc/options
changeset 74347 f984d30cd0c3
parent 73872 ced6e3c03425
child 76578 06b001094ddb