From 1c44e861bea6069ab9619b6f84065db59fad042b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 29 Jan 2023 14:07:21 +0100
Subject: [PATCH] fix: search.html for relative roots

---
 DocGen4/Output/Template.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
index ecff70c..a77343a 100644
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@@ -48,7 +48,7 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
           <form action="https://google.com/search" method="get" id="search_form">
             <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib4_docs"/>
             <input type="text" name="q" autocomplete="off"/>&#32;
-            <button id="search_button" onclick="javascript: form.action='/search.html';">Search</button>
+            <button id="search_button" onclick={s!"javascript: form.action='{← getRoot}search.html';"}>Search</button>
             <button>Google site search</button>
           </form>
         </header>