src/Tools/jEdit/etc/settings
changeset 68575 d40d03487f64
parent 66906 03a96b8c7c06
child 70220 089753519be0