| Index: editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/DartCore.java
|
| diff --git a/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/DartCore.java b/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/DartCore.java
|
| index 74f47df4d6c92b8404be97591eafe3e633503b02..bd14b70d802b8ff4408fb40144a7b3b36ea3c59f 100644
|
| --- a/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/DartCore.java
|
| +++ b/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/DartCore.java
|
| @@ -1737,6 +1737,12 @@ public class DartCore extends Plugin implements DartSdkListener {
|
| return DartCore.getPlugin().getPrefs().getBoolean(ENABLE_HINTS_PREFERENCE, true);
|
| }
|
|
|
| + public boolean isLintsEnabled() {
|
| + // TODO (pquitslund) not yet implemented
|
| +// return DartCore.getPlugin().getPrefs().getBoolean(ENABLE_LINTS_PREFERENCE, true);
|
| + return false;
|
| + }
|
| +
|
| /**
|
| * Save the core plugin preferences
|
| *
|
|
|