src/Tools/jEdit/etc/settings
changeset 49295 2750756db9c5
parent 47235 a92d3620e156
child 49612 e6a53d203362
equal deleted inserted replaced
49294:a600c017f814 49295:2750756db9c5