diff --git a/edit/codemirror-editing-hooks.js b/edit/codemirror-editing-hooks.js
index 3a8d436f..ac04b275 100644
--- a/edit/codemirror-editing-hooks.js
+++ b/edit/codemirror-editing-hooks.js
@@ -19,6 +19,9 @@ onDOMscriptReady('/codemirror.js').then(() => {
     nextEditor, prevEditor,
     commentSelection,
   };
+  const ORIGINAL_COMMANDS = {
+    insertTab: CodeMirror.commands.insertTab,
+  };
   // reroute handling to nearest editor when keypress resolves to one of these commands
   const REROUTED = new Set([
     'save',
@@ -244,6 +247,12 @@ onDOMscriptReady('/codemirror.js').then(() => {
         CodeMirror.setOption('indentUnit', value);
         break;
 
+      case 'indentWithTabs':
+        CodeMirror.commands.insertTab = value ?
+          ORIGINAL_COMMANDS.insertTab :
+          CodeMirror.commands.insertSoftTab;
+        break;
+
       case 'theme': {
         const themeLink = $('#cm-theme');
         // use non-localized 'default' internally