pref: prefetch search data

2022-02-20 23:05:35 +08:00 · 2022-02-20 23:05:35 +08:00 · b9c5109aaf
parent 9f13773a7d
commit b9c5109aaf
1 changed files with 1 additions and 0 deletions
--- a/DocGen4/Output/Template.lean
+++ b/DocGen4/Output/Template.lean
@ -18,6 +18,7 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
        <link rel="stylesheet" href={s!"{←getRoot}style.css"}/>
        <link rel="stylesheet" href={s!"{←getRoot}pygments.css"}/>
        <link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>
+        <link rel="prefetch" href={s!"{←getRoot}searchable_data.json"}/>
        <title>{title}</title>
        <meta charset="UTF-8"/>
        <meta name="viewport" content="width=device-width, initial-scale=1"/>