help.html: add null check

diff --git a/basis/help/html/html.factor b/basis/help/html/html.factor
index ce4c206eaca45d8872154eb498ebbbfbe04bd7d3..fd258fe2d696ce2539205a380511b4dbd9ca497a 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');
         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().select()
+                        }, 0);
+                    }

                 }
             }
         });
                 }
             }
         });

diff --git a/extra/webapps/help/search.js b/extra/webapps/help/search.js
index db99569fc4e834bd9bccfa455f364855936f3ec2..7ad98c8160029921fa82409d1b6e4c244e50e408 100644 (file)
--- a/extra/webapps/help/search.js
+++ b/extra/webapps/help/search.js
@@ -8,11 +8,13 @@ window.onload = function() {
 document.addEventListener('keydown', function (event) {
     if (event.code == 'Slash') {
         let input = document.getElementById('search');
 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().select()
+                }, 0);
+            }

         }
     }
 });
         }
     }
 });