fix: missed .raw annotation for scripts

leanprover · Jun 17, 2024 · c5f9e71 · c5f9e71
1 parent 50b0f4d
commit c5f9e71
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/DocGen4/Output/Search.lean b/DocGen4/Output/Search.lean
@@ -11,8 +11,8 @@ namespace Output
 
 open scoped DocGen4.Jsx
 
-def search : BaseHtmlM Html := do templateExtends (baseHtml "Search") <|
-  pure <|
+def search : BaseHtmlM Html := do templateExtends (baseHtml "Search") <| do
+  pure
     <main>
       <h1> Search Results </h1>
       <label for="search_page_query">Query:</label>
@@ -36,9 +36,9 @@ def search : BaseHtmlM Html := do templateExtends (baseHtml "Search") <|
         <input type="checkbox" id="opaque_checkbox" class="kind_checkbox" value="opaque" checked="checked" />
         <label for="opaque_checkbox">opaque</label>
       </div>
-      
+
       <script>
-        document.getElementById("search_page_query").value = new URL(window.location.href).searchParams.get("q")
+        {.raw "document.getElementById('search_page_query').value = new URL(window.location.href).searchParams.get('q')"}
       </script>
       <div id="search_results">
       </div>