2002-07-08 15:43:20 +00:00
|
|
|
#
|
|
|
|
|
# Plugin properties
|
|
|
|
|
#
|
2002-07-08 17:24:35 +00:00
|
|
|
plugin.net.sourceforge.pmd.jedit.PMDJEditPlugin.name=PMD
|
2002-07-08 15:43:20 +00:00
|
|
|
plugin.net.sourceforge.pmd.jedit.PMDJEditPlugin.author=Tom Copeland
|
2002-07-22 19:59:04 +00:00
|
|
|
plugin.net.sourceforge.pmd.jedit.PMDJEditPlugin.version=0.5
|
2002-07-08 15:43:20 +00:00
|
|
|
plugin.net.sourceforge.pmd.jedit.PMDJEditPlugin.docs=jedit.html
|
|
|
|
|
plugin.net.sourceforge.pmd.jedit.PMDJEditPlugin.depend.0=jdk 1.3
|
|
|
|
|
plugin.net.sourceforge.pmd.jedit.PMDJEditPlugin.depend.1=jedit 04.00.99.00
|
2002-07-18 16:46:35 +00:00
|
|
|
plugin.net.sourceforge.pmd.jedit.PMDJEditPlugin.jars=pmd-0.6.jar
|
2002-07-08 15:43:20 +00:00
|
|
|
|
|
|
|
|
#
|
|
|
|
|
# Menu properties
|
|
|
|
|
#
|
2002-07-22 19:57:18 +00:00
|
|
|
PMD.label=$PMD
|
2002-07-09 17:20:08 +00:00
|
|
|
|
2002-07-22 19:57:18 +00:00
|
|
|
#
|
|
|
|
|
# Option pane properties
|
|
|
|
|
#
|
|
|
|
|
options.pmd.title=PMD
|
2002-07-09 17:20:08 +00:00
|
|
|
options.pmd.label=PMD
|
|
|
|
|
|
