| Index: editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/AnalysisMarkerManager.java
|
| diff --git a/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/AnalysisMarkerManager.java b/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/AnalysisMarkerManager.java
|
| index b282a7892c73fa92f2f59854f4fc85008700681d..29db80863bf2af4724eb30793521d1ef8f057c5c 100644
|
| --- a/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/AnalysisMarkerManager.java
|
| +++ b/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/AnalysisMarkerManager.java
|
| @@ -133,6 +133,7 @@ public class AnalysisMarkerManager {
|
| marker.setAttribute(IMarker.LINE_NUMBER, lineNum);
|
| marker.setAttribute(ERROR_CODE, encodeErrorCode(errorCode));
|
| marker.setAttribute(IMarker.MESSAGE, error.getMessage());
|
| + marker.setAttribute(DartCore.MARKER_ATTR_CORRECTION, error.getCorrection());
|
|
|
| if (isHint) {
|
| marker.setAttribute(IMarker.PRIORITY, IMarker.PRIORITY_HIGH);
|
|
|