help.html: only input.focus().

[factor.git] / basis / help / html / html.factor

diff --git a/basis/help/html/html.factor b/basis/help/html/html.factor
index ce4c206eaca45d8872154eb498ebbbfbe04bd7d3..c9cd833b69c4888f60413f4eabd20081a499c475 100644 (file)
--- a/basis/help/html/html.factor
+++ b/basis/help/html/html.factor
@@ -97,11 +97,13 @@ M: pathname url-of
         document.addEventListener('keydown', function (event) {
             if (event.code == 'Slash') {
                 let input = document.getElementById('search');
-                if (input !== document.activeElement) {
-                    event.preventDefault();
-                    setTimeout(function() {
-                        input.focus().select()
-                    }, 0);
+                if (input != null) {
+                    if (input !== document.activeElement) {
+                        event.preventDefault();
+                        setTimeout(function() {
+                            input.focus();
+                        }, 0);
+                    }
                 }
             }
         });