| Index: editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/DartCoreDebug.java
|
| diff --git a/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/DartCoreDebug.java b/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/DartCoreDebug.java
|
| index ff666845266bc4054b8f0e587b3a246443df152a..54680256bd9e8873bd8fbb9591bc1bb601b4ea8b 100644
|
| --- a/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/DartCoreDebug.java
|
| +++ b/editor/tools/plugins/com.google.dart.tools.core/src/com/google/dart/tools/core/DartCoreDebug.java
|
| @@ -35,7 +35,6 @@ public class DartCoreDebug {
|
| public static final boolean TRACE_INDEX_PROCESSOR = isOptionTrue("trace/index/processor");
|
|
|
| public static final boolean ENABLE_CONTENT_ASSIST_TIMING = isOptionTrue("debug/ResultCollector");
|
| - public static final boolean ENABLE_TYPE_REFINEMENT = isOptionTrue("debug/RefineTypes");
|
| public static final boolean ENABLE_MARK_OCCURRENCES = isOptionTrue("debug/markOccurrences");
|
|
|
| // Performance measurement and reporting options.
|
|
|