src/Tools/jEdit/etc/options
changeset 66787 64b47495676d
parent 66180 201d42f67bba
child 67322 734a4e44b159