| Index: devtools.js | 
| =================================================================== | 
| --- a/devtools.js | 
| +++ b/devtools.js | 
| @@ -39,18 +39,21 @@ | 
| panelWindow = window; | 
| }); | 
| panel.onHidden.addListener(window => | 
| { | 
| panelWindow = null; | 
| }); | 
| - panel.onSearch.addListener((eventName, queryString) => | 
| + if (panel.onSearch) | 
| { | 
| - if (panelWindow) | 
| - panelWindow.postMessage({type: eventName, queryString}, "*"); | 
| - }); | 
| + panel.onSearch.addListener((eventName, queryString) => | 
| + { | 
| + if (panelWindow) | 
| + panelWindow.postMessage({type: eventName, queryString}, "*"); | 
| + }); | 
| + } | 
| } | 
| ); | 
| } | 
| } | 
| ); |