src/Tools/jEdit/etc/options
changeset 65482 721feefce9c6
parent 65141 c706b57b1694
child 66158 ad83d4971dfe