help.html: whoops, typo
authorJohn Benediktsson <mrjbq7@gmail.com>
Sun, 25 Sep 2022 20:58:34 +0000 (13:58 -0700)
committerJohn Benediktsson <mrjbq7@gmail.com>
Sun, 25 Sep 2022 20:58:34 +0000 (13:58 -0700)
basis/help/html/html.factor

index fd258fe2d696ce2539205a380511b4dbd9ca497a..77d75e9aa73430cd5da5266e36d9a7e80ce6c5ec 100644 (file)
@@ -98,7 +98,7 @@ M: pathname url-of
             if (event.code == 'Slash') {
                 let input = document.getElementById('search');
                 if (input != null) {
-                    if input !== document.activeElement) {
+                    if (input !== document.activeElement) {
                         event.preventDefault();
                         setTimeout(function() {
                             input.focus().select()