Skip to main content
diff options
Diffstat (limited to 'org.eclipse.ui.editors/')
1 files changed, 1 insertions, 0 deletions
diff --git a/org.eclipse.ui.editors/ b/org.eclipse.ui.editors/
index 15a15536b1d..42b9b6ea423 100644
--- a/org.eclipse.ui.editors/
+++ b/org.eclipse.ui.editors/
@@ -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

Back to the top