- let keycode = e.which;
-
- if (keycode == 27) { // escape and drop prefix
- hotkey_prefix = false;
- }
-
- if (keycode == 16 || keycode == 17) return; // ignore lone shift / ctrl
-
- const hotkeys = getInitParam("hotkeys");
- const keychar = String.fromCharCode(keycode).toLowerCase();
-
- if (!hotkey_prefix && hotkeys[0].indexOf(keychar) != -1) {
-
- const date = new Date();
- const ts = Math.round(date.getTime() / 1000);
-
- hotkey_prefix = keychar;
- hotkey_prefix_pressed = ts;
-
- $("cmdline").innerHTML = keychar;
- Element.show("cmdline");
-
- e.stopPropagation();