diff options
Diffstat (limited to 'org.eclipse.ui.editors/plugin.properties')
| -rw-r--r-- | org.eclipse.ui.editors/plugin.properties | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/org.eclipse.ui.editors/plugin.properties b/org.eclipse.ui.editors/plugin.properties index 15a15536b1d..42b9b6ea423 100644 --- a/org.eclipse.ui.editors/plugin.properties +++ b/org.eclipse.ui.editors/plugin.properties @@ -120,6 +120,7 @@ preferenceKeywords.general= pop-up text editor tabs spaces undo history ruler ov preferenceKeywords.tabWidth= tab width preferenceKeywords.lineNumber= line numbers preferenceKeywords.printMargin= print margin +preferenceKeywords.annotationCodeMining= annotation code mining marker error warning info preferenceKeywords.annotations= annotations vertical ruler overview colors text editor preferenceKeywords.quickdiff= quick diff compare reference colors text editor changes preferenceKeywords.accessibility= accessibility caret cursor quick diff text editor ruler |