src/Tools/jEdit/etc/settings
changeset 44630 d08cb39b628a
parent 43671 a250b092ac66
child 44956 01a1b3b3341f