one more

leanprover · Jun 10, 2024 · ab34802 · ab34802
1 parent 2f52da7
commit ab34802
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
@@ -17,7 +17,7 @@ The HTML template used for all pages.
 def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do
   let moduleConstant :=
     if let some module := ← getCurrentName then
-      #[<script>{s!"const MODULE_NAME={String.quote module.toString};"}</script>]
+      #[<script>{.raw s!"const MODULE_NAME={String.quote module.toString};"}</script>]
     else
       #[]
   pure