editor: convert string to int; fixes #102
This commit is contained in:
parent
5485fbf8b3
commit
028ac1d299
2
edit.js
2
edit.js
|
@ -291,7 +291,7 @@ function acmeEventListener(event) {
|
||||||
var value = el.type == "checkbox" ? el.checked : el.value;
|
var value = el.type == "checkbox" ? el.checked : el.value;
|
||||||
switch (option) {
|
switch (option) {
|
||||||
case "tabSize":
|
case "tabSize":
|
||||||
CodeMirror.setOption("indentUnit", value);
|
CodeMirror.setOption("indentUnit", Number(value));
|
||||||
break;
|
break;
|
||||||
case "theme":
|
case "theme":
|
||||||
var themeLink = document.getElementById("cm-theme");
|
var themeLink = document.getElementById("cm-theme");
|
||||||
|
|
Loading…
Reference in New Issue
Block a user