IdrisDoc, set charset and viewport
The meta-charset tag ensures that the charset is correclty detected even
if the HTTP Server is misconfigured or BOMs stripped.
The meta-viewport tag makes the documentation work on mobile devices and
tablets.
commit48fa7450227c61d23d825eff771e52c4fd3ff5a7
authorReiner Dolp <reiner-dolp@users.noreply.github.com>
dateSun 29 Oct 2017, 22:43 (9 years ago)
parent2eec999
src/Idris/IdrisDoc.hs+2
@@ -641,6 +641,8 @@ wrapper ns inner =
641641 indexPage = base ++ "index.html" :: String
642642 in H.docTypeHtml $ do
643643 H.head $ do
644+ H.meta ! charset "utf-8"
645+ H.meta ! name "viewport" ! content "width=device-width, initial-scale=1, shrink-to-fit=no"
644646 H.title $ do
645647 "IdrisDoc"
646648 if index then " Index" else do