Added ignorecase to editor

This commit is contained in:
Jamie Peabody
2017-02-28 22:32:46 +00:00
parent d761609e54
commit da41c28fdb
3 changed files with 14 additions and 3 deletions

View File

@@ -140,6 +140,7 @@ if (isset($_GET['debug'])) {
<ul>
<li id="options-wrap">Wrap lines</li>
<li id="options-ignorews">Ignore white space</li>
<li id="options-ignorecase">Ignore case</li>
<li class="separator"></li>
<li id="options-viewport" title="Improves performance for large files">Enable viewport</li>
<li id="options-sidebars" title="Improves performance for large files">Enable side bars</li>