fix: get rid of double <h1> around page titles

leanprover · Jan 10, 2024 · 45ded44 · 45ded44
1 parent 9e46814
commit 45ded44
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/verso-blog/Verso/Genre/Blog/Generate.lean b/src/verso-blog/Verso/Genre/Blog/Generate.lean
@@ -52,7 +52,7 @@ namespace Template
 
 namespace Params
 def forPart [BlogGenre g] [GenreHtml g IO] [ToHtml g IO (Part g)] (txt : Part g) : GenerateM Params := do
-  let titleHtml := {{ <h1> {{ ← txt.title.mapM (GenerateM.toHtml g) }} </h1>}}
+  let titleHtml : Html ← txt.title.mapM (GenerateM.toHtml g)
   let preamble ← txt.content.mapM (GenerateM.toHtml g)
   let subParts ← txt.subParts.mapM (GenerateM.toHtml g)
   return ofList [