|  |  | @@ -4912,6 +4912,10 @@ document.addEventListener("DOMContentLoaded", () => { | 
		
	
		
			
			|  |  |  | .querySelector("#search-box") | 
		
	
		
			
			|  |  |  | .addEventListener("change", (e) => doSearch(e.target.value)); | 
		
	
		
			
			|  |  |  | 
 | 
		
	
		
			
			|  |  |  | 
 | 
		
	
		
			
			|  |  |  | document | 
		
	
		
			
			|  |  |  | .querySelector("#search-box") | 
		
	
		
			
			|  |  |  | .addEventListener("keydown", e => e.stopPropagation()); | 
		
	
		
			
			|  |  |  | // Webkit doesn't draw resized SVGs correctly. It will always draw them at their intrinsic size, I think | 
		
	
		
			
			|  |  |  | // This checks for that. | 
		
	
		
			
			|  |  |  | webkitBugTest.onload = () => { | 
		
	
	
		
			
				|  |  | 
 |