src/Tools/jEdit/etc/options
changeset 57881 37920df63ab9
parent 57425 625a369b4f32
child 57833 2c2bae3da1c2