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 |