| Index: editor/tools/plugins/com.google.dart.tools.ui/.options
|
| diff --git a/editor/tools/plugins/com.google.dart.tools.ui/.options b/editor/tools/plugins/com.google.dart.tools.ui/.options
|
| new file mode 100644
|
| index 0000000000000000000000000000000000000000..aea667d0caaca63e97672f94faaf2be4fe428a9b
|
| --- /dev/null
|
| +++ b/editor/tools/plugins/com.google.dart.tools.ui/.options
|
| @@ -0,0 +1,10 @@
|
| +#
|
| +# Internal options for the Dart UI
|
| +#
|
| +# To run Dart Editor with custom options,
|
| +# copy one or more of these settings to an options file
|
| +# then launch Dart Editor from the command line with
|
| +#
|
| +# -debug /path/to/options/file
|
| +#
|
| +com.google.dart.tools.ui/experimental/useOnlySemanticHighlighter = false
|
|
|