| Index: editor/tools/plugins/com.google.dart.tools.core/.options
|
| ===================================================================
|
| --- editor/tools/plugins/com.google.dart.tools.core/.options (revision 3005)
|
| +++ editor/tools/plugins/com.google.dart.tools.core/.options (working copy)
|
| @@ -3,6 +3,7 @@
|
| com.google.dart.tools.core/debug/frog = false
|
| com.google.dart.tools.core/debug/metrics = false
|
| com.google.dart.tools.core/debug/warmup = false
|
| +com.google.dart.tools.core/debug/verbose = false
|
| com.google.dart.tools.core/bleedingEdge = false
|
| com.google.dart.tools.core/deployFrog = false
|
|
|
|
|