src/Tools/jEdit/etc/settings
changeset 45455 4f974c0c5c2f
parent 45057 86c9b73158a8
child 45636 202071bb7f86
equal deleted inserted replaced
45454:388fb71623dd 45455:4f974c0c5c2f