From 028ac1d299d816a125b8e336c33dc089c6805fdb Mon Sep 17 00:00:00 2001
From: tophf <tophf@gmx.com>
Date: Wed, 21 Jun 2017 22:05:21 +0300
Subject: [PATCH] editor: convert string to int; fixes #102

---
 edit.js | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/edit.js b/edit.js
index f100b177..f8e2cd01 100644
--- a/edit.js
+++ b/edit.js
@@ -291,7 +291,7 @@ function acmeEventListener(event) {
 	var value = el.type == "checkbox" ? el.checked : el.value;
 	switch (option) {
 		case "tabSize":
-			CodeMirror.setOption("indentUnit", value);
+			CodeMirror.setOption("indentUnit", Number(value));
 			break;
 		case "theme":
 			var themeLink = document.getElementById("cm-theme");