Add search to docs

Closes: #295
This commit is contained in:
Eike Kettner
2020-09-30 00:17:18 +02:00
parent f40eb15e86
commit 9f1d8cee8f
16 changed files with 422 additions and 123 deletions

View File

@ -0,0 +1,16 @@
<script>
var initSearch = function() {
var elmSearch = Elm.Search.init({
node: document.getElementById("search"),
flags: {}
});
initElmSearch(elmSearch);
}
if (document.readyState === "complete" ||
(document.readyState !== "loading" && !document.documentElement.doScroll)
) {
initSearch();
} else {
document.addEventListener("DOMContentLoaded", initSearch);
}
</script>