src/Tools/jEdit/etc/settings
changeset 45455 4f974c0c5c2f
parent 45057 86c9b73158a8
child 45636 202071bb7f86