@@ -363,7 +363,7 @@ window.search = window.search || {};
363363            } 
364364        } 
365365    } 
366-      
366+ 
367367    function  showSearch ( yes )  { 
368368        if  ( yes )  { 
369369            search_wrap . classList . remove ( 'hidden' ) ; 
@@ -441,7 +441,6 @@ window.search = window.search || {};
441441    } 
442442
443443    function  doSearch ( searchterm )  { 
444- 
445444        // Don't search the same twice 
446445        if  ( current_searchterm  ==  searchterm )  {  return ;  } 
447446        else  {  current_searchterm  =  searchterm ;  } 
@@ -468,15 +467,18 @@ window.search = window.search || {};
468467        showResults ( true ) ; 
469468    } 
470469
471-     fetch ( '{{ resource "searchindex.json" }}' ) 
472-         . then ( response  =>  response . json ( ) ) 
473-         . then ( json  =>  init ( json ) )         
474-         . catch ( error  =>  {  // Try to load searchindex.js if fetch failed 
475-             var  script  =  document . createElement ( 'script' ) ; 
476-             script . src  =  '{{ resource "searchindex.js" }}' ; 
477-             script . onload  =  ( )  =>  init ( window . search ) ; 
478-             document . head . appendChild ( script ) ; 
479-         } ) ; 
470+     function  loadScript ( url ,  id )  { 
471+         const  script  =  document . createElement ( 'script' ) ; 
472+         script . src  =  '{{ resource "searchindex.js" }}' ; 
473+         script . id  =  id ; 
474+         script . onload  =  ( )  =>  init ( window . search ) ; 
475+         script . onerror  =  error  =>  { 
476+             console . error ( `Failed to load \`${ url } ${ error }  ) ;     
477+         } ; 
478+         document . head . append ( script ) ; 
479+     } 
480+ 
481+     loadScript ( '{{ resource "searchindex.js" }}' ,  'search-index' ) ; 
480482
481483    // Exported functions 
482484    search . hasFocus  =  hasFocus ; 
0 commit comments