src/Tools/jEdit/etc/options
changeset 60842 5510c8444bc4
parent 59753 d743e0e53f41
child 60876 52edced9cce5