diff --git a/edit.html b/edit.html
index c870246d..25e1d98e 100644
--- a/edit.html
+++ b/edit.html
@@ -138,7 +138,7 @@
-
+
diff --git a/edit/codemirror-editing-hooks.js b/edit/codemirror-editing-hooks.js
index 4cc4a104..f01c5eb1 100644
--- a/edit/codemirror-editing-hooks.js
+++ b/edit/codemirror-editing-hooks.js
@@ -13,7 +13,6 @@ onDOMscriptReady('/codemirror.js').then(() => {
save,
toggleStyle,
jumpToLine,
- defocusEditor,
nextEditor, prevEditor,
};
// reroute handling to nearest editor when keypress resolves to one of these commands
@@ -149,10 +148,6 @@ onDOMscriptReady('/codemirror.js').then(() => {
return this.display.wrapper.parentNode;
}
- function defocusEditor(cm) {
- cm.display.input.blur();
- }
-
function nextEditor(cm) {
return nextPrevEditor(cm, 1);
}
@@ -513,7 +508,8 @@ onDOMscriptReady('/codemirror.js').then(() => {
el._hotkeyTooltipKeyMap = mapName;
const title = el._hotkeyTooltipTitle = el._hotkeyTooltipTitle || el.title;
const cmd = el.dataset.hotkeyTooltip;
- const key = findKeyForCommand(cmd, mapName) ||
+ const key = cmd[0] === '=' ? cmd.slice(1) :
+ findKeyForCommand(cmd, mapName) ||
extraKeys && findKeyForCommand(cmd, extraKeys);
const newTitle = title + (title && key ? '\n' : '') + (key || '');
if (el.title !== newTitle) el.title = newTitle;