| Index: editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/AnalysisMarkerManager_NEW.java
|
| diff --git a/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/AnalysisMarkerManager_NEW.java b/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/AnalysisMarkerManager_NEW.java
|
| index 78129fa9d399b6d5facf5933b964454f5efa6ad7..9b43a69b869fce6aa79d56d3fd36f5d9fa51a696 100644
|
| --- a/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/AnalysisMarkerManager_NEW.java
|
| +++ b/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/internal/builder/AnalysisMarkerManager_NEW.java
|
| @@ -126,6 +126,7 @@ public class AnalysisMarkerManager_NEW {
|
| marker.setAttribute(IMarker.CHAR_END, location.getOffset() + location.getLength());
|
| marker.setAttribute(IMarker.LINE_NUMBER, location.getStartLine());
|
| marker.setAttribute(IMarker.MESSAGE, error.getMessage());
|
| + marker.setAttribute(DartCore.MARKER_ATTR_CORRECTION, error.getCorrection());
|
|
|
| if (isHint) {
|
| marker.setAttribute(IMarker.PRIORITY, IMarker.PRIORITY_HIGH);
|
|
|