src/Tools/jEdit/etc/settings
changeset 46088 948bef826443
parent 45636 202071bb7f86
child 47063 effcfa38e77b
equal deleted inserted replaced
46087:680edc162249 46088:948bef826443