Fuzzy search of docs (#1007)

Author: Roy-Orbison

include/footer.inc

@@ -99,7 +99,7 @@ if (!empty($_SERVER['BASE_PAGE'])
  <!-- External and third party libraries. -->
  <script src="https://code.jquery.com/jquery-3.6.0.min.js" integrity="sha256-/xUj+3OJU5yExlq6GSYGSHk7tPXikynS7ogEvDej/m4=" crossorigin="anonymous"></script>
 <?php
- $jsfiles = ["ext/hogan-3.0.2.min.js", "ext/typeahead.min.js", "ext/mousetrap.min.js", "ext/jquery.scrollTo.min.js", "search.js", "common.js"];
+ $jsfiles = ["ext/hogan-3.0.2.min.js", "ext/typeahead.jquery.min.js", "ext/FuzzySearch.min.js", "ext/mousetrap.min.js", "ext/jquery.scrollTo.min.js", "search.js", "common.js"];
  foreach ($jsfiles as $filename) {
    $path = dirname(__DIR__) . '/js/' . $filename;
    echo '<script src="/cached.php?t=' . @filemtime($path) . '&amp;f=/js/' . $filename . '"></script>' . "\n";