| Index: editor/tools/plugins/com.google.dart.tools.deploy/plugin.xml
|
| diff --git a/editor/tools/plugins/com.google.dart.tools.deploy/plugin.xml b/editor/tools/plugins/com.google.dart.tools.deploy/plugin.xml
|
| index f46c487b8b288383b268d997b72795908d1b4503..7e4e92d88ec9a74ea280ff1abca5f58c76ba014a 100644
|
| --- a/editor/tools/plugins/com.google.dart.tools.deploy/plugin.xml
|
| +++ b/editor/tools/plugins/com.google.dart.tools.deploy/plugin.xml
|
| @@ -423,16 +423,16 @@
|
|
|
| <extension-point id="com.google.dart.tools.ui.theme.mapper" name="Editor Mapping" schema="schema/com.google.dart.tools.ui.theme.mapper.exsd"/>
|
| <extension-point id="com.google.dart.tools.ui.theme.theme" name="Color Theme" schema="schema/com.google.dart.tools.ui.theme.theme.exsd"/>
|
| -<!--
|
| +
|
| <extension
|
| point="org.eclipse.ui.preferencePages">
|
| <page
|
| class="com.google.dart.tools.ui.theme.preferences.ThemePreferencePage"
|
| id="com.google.dart.tools.ui.theme.preferences.ThemePreferencePage"
|
| - name="Color Theme">
|
| + name="Visual Theme">
|
| </page>
|
| </extension>
|
| --->
|
| +
|
| <extension
|
| point="org.eclipse.core.runtime.preferences">
|
| <initializer
|
|
|