src/Tools/jEdit/etc/options
changeset 53748 be0ddf3dd01b
parent 53715 68c664737d04
child 53884 48d13465c7c7