src/Tools/jEdit/etc/options
changeset 66676 39db5bb7eb0a
parent 66180 201d42f67bba
child 67322 734a4e44b159