From 7754c8f20c151a9222dac31af255f6ed962f8eb0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 25 Dec 2024 21:25:19 +0100
Subject: [PATCH] chore: kill the google button

---
 DocGen4/Output/Template.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index e145eaec..921100fd 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -47,11 +47,9 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
         <header>
           <h1><label for="nav_toggle"></label><span>Documentation</span></h1>
           <h2 class="header_filename break_within">[breakWithin title]</h2>
-          <form action="https://google.com/search" method="get" id="search_form">
-            <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib4_docs"/>
+          <form id="search_form">
             <input type="text" name="q" autocomplete="off"/>{.raw "&#32;"}
             <button id="search_button" onclick={s!"javascript: form.action='{← getRoot}search.html';"}>Search</button>
-            <button>Google site search</button>
           </form>
         </header>