From e906f1a60534559edd689711bee8d409b1b38454 Mon Sep 17 00:00:00 2001
From: Marcel Gerber <mg.hain@gmx.de>
Date: Sat, 20 Dec 2014 13:24:11 +0100
Subject: [PATCH] Handle undefined theme the right way

---
 src/view/ThemeManager.js | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/view/ThemeManager.js b/src/view/ThemeManager.js
index d546849a3f2..3d5450522ce 100644
--- a/src/view/ThemeManager.js
+++ b/src/view/ThemeManager.js
@@ -266,10 +266,8 @@ define(function (require, exports, module) {
             var cm = editor._codeMirror;
             ThemeView.updateThemes(cm);
 
-            // currentTheme can be undefined if you reloaded without extensions
-            if (currentTheme && currentTheme.addModeClass !== undefined) {
-                cm.setOption("addModeClass", currentTheme.addModeClass);
-            }
+            // currentTheme can be undefined, so watch out
+            cm.setOption("addModeClass", !!(currentTheme && currentTheme.addModeClass));
         });
     }