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 a6e911b73b4c5d5a4176e55fbe2870814d28ca7f..26f4f6921d1e1905e62e7e57172d51190c751a02 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 |
@@ -171,6 +171,11 @@ public class DartCore extends Plugin implements DartSdkListener { |
public static final String ANGULAR_WARNING_MARKER_TYPE = PLUGIN_ID + ".angular_warning"; |
/** |
+ * Correction marker attribute. |
+ */ |
+ public static final String MARKER_ATTR_CORRECTION = "correction"; |
+ |
+ /** |
* Extension for single unit compiled into JavaScript. |
*/ |
public static final String EXTENSION_JS = "js"; |