src/Tools/jEdit/etc/settings
changeset 68743 91162dd89571
parent 66906 03a96b8c7c06
child 70220 089753519be0