src/Tools/jEdit/etc/options
changeset 68743 91162dd89571
parent 67322 734a4e44b159
child 68871 f5c76072db55