src/Tools/jEdit/etc/options
changeset 59009 348561aa3869
parent 58750 1b4b005d73c1
child 59120 74fde39274d5