chore: kill the google button

leanprover · Dec 25, 2024 · 7754c8f · 7754c8f
1 parent fd52917
commit 7754c8f
Showing 1 changed file with 1 addition and 3 deletions.
diff --git 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>