| Index: editor/tools/plugins/com.google.dart.tools.core/.options
|
| diff --git a/editor/tools/plugins/com.google.dart.tools.core/.options b/editor/tools/plugins/com.google.dart.tools.core/.options
|
| index e95b4bb18bdca03c08149e3e8585a78a7156317c..0dd4145f9a6a28747914166fb66387710b29af7f 100644
|
| --- a/editor/tools/plugins/com.google.dart.tools.core/.options
|
| +++ b/editor/tools/plugins/com.google.dart.tools.core/.options
|
| @@ -30,4 +30,3 @@ com.google.dart.tools.core/trace/index/processor = false
|
| com.google.dart.tools.core/perf/index = false
|
|
|
| com.google.dart.tools.core/debug/markOccurrences = false
|
| -com.google.dart.tools.core/debug/RefineTypes = false
|
|
|