From 74ef2f6fcf8eacf4514fdc43b0c158153354e5ea Mon Sep 17 00:00:00 2001
From: tophf <tophf@gmx.com>
Date: Tue, 3 Jul 2018 08:42:13 +0300
Subject: [PATCH] editors isn't defined on some pages like install-usercss

fixes #411
---
 edit/codemirror-default.js | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/edit/codemirror-default.js b/edit/codemirror-default.js
index 90215a8a..9401a32d 100644
--- a/edit/codemirror-default.js
+++ b/edit/codemirror-default.js
@@ -229,7 +229,7 @@
   });
 
   // doubleclick option
-  {
+  if (window.editors) {
     const fn = (cm, repeat) =>
       repeat === 'double' ?
         {unit: selectTokenOnDoubleclick} :