src/Tools/jEdit/etc/options
changeset 65361 ecefb68dc21d
parent 65141 c706b57b1694
child 66158 ad83d4971dfe