diff --git a/util/gh-pages/index.html b/util/gh-pages/index.html index 0c0f28e4fbd3..7f271ac83859 100644 --- a/util/gh-pages/index.html +++ b/util/gh-pages/index.html @@ -541,7 +541,7 @@

Clippy Lints

- diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js index 661f80a6d346..ba13cc40cb1d 100644 --- a/util/gh-pages/script.js +++ b/util/gh-pages/script.js @@ -579,6 +579,32 @@ function setTheme(theme, store) { } } +function handleShortcut(ev) { + if (ev.ctrlKey || ev.altKey || ev.metaKey) { + return; + } + + if (document.activeElement.tagName === "INPUT") { + if (ev.key === "Escape") { + document.activeElement.blur(); + } + } else { + switch (ev.key) { + case "s": + case "S": + case "/": + ev.preventDefault(); // To prevent the key to be put into the input. + document.getElementById("search-input").focus(); + break; + default: + break; + } + } +} + +document.addEventListener("keypress", handleShortcut); +document.addEventListener("keydown", handleShortcut); + // loading the theme after the initial load const prefersDark = window.matchMedia("(prefers-color-scheme: dark)"); const theme = localStorage.getItem('clippy-lint-list-theme');