src/Tools/jEdit/etc/settings
changeset 61726 04f8564d6983
parent 61148 b3efd7552d83
child 61974 5b067c681989