src/Tools/jEdit/etc/options
changeset 67588 f3a68e350ab6
parent 67322 734a4e44b159
child 68871 f5c76072db55