Fix: remove unneeded comment

This commit is contained in:
eight 2018-09-01 21:23:12 +08:00
parent ca5c0e92cd
commit f5ea73caeb
2 changed files with 0 additions and 2 deletions

View File

@ -25,7 +25,6 @@
<script src="js/script-loader.js"></script> <script src="js/script-loader.js"></script>
<script src="js/storage-util.js"></script> <script src="js/storage-util.js"></script>
<script src="content/apply.js"></script> <script src="content/apply.js"></script>
<!-- <script src="edit/lint.js"></script> -->
<script src="edit/util.js"></script> <script src="edit/util.js"></script>
<script src="edit/regexp-tester.js"></script> <script src="edit/regexp-tester.js"></script>
<script src="edit/applies-to-line-widget.js"></script> <script src="edit/applies-to-line-widget.js"></script>

View File

@ -582,7 +582,6 @@ function showCodeMirrorPopup(title, html, options) {
foldGutter: true, foldGutter: true,
gutters: ['CodeMirror-linenumbers', 'CodeMirror-foldgutter', 'CodeMirror-lint-markers'], gutters: ['CodeMirror-linenumbers', 'CodeMirror-foldgutter', 'CodeMirror-lint-markers'],
matchBrackets: true, matchBrackets: true,
// lint: linterConfig.getForCodeMirror(),
styleActiveLine: true, styleActiveLine: true,
theme: prefs.get('editor.theme'), theme: prefs.get('editor.theme'),
keyMap: prefs.get('editor.keyMap') keyMap: prefs.get('editor.keyMap')