src/Tools/jEdit/jedit_main/plugin.props
changeset 76926 d858e6f15da3
parent 76390 5309f1283d93
child 78593 55ca7578d3e9