search: link to "pretty" URLs

One of GitHub Pages' nice features is that you do not have to append
`.html` to the URLs. For example, the following two URLs refer to the
same page:

- https://git-for-windows.github.io/requirements

- https://git-for-windows.github.io/requirements.html

We use this feature in the migration of Git's home page to a static
website, to maintain backwards-compatibility with the Rails app:
Navigating to /docs/git-config will automatically load
/docs/git-config.html.

Pagefind knows nothing about this, of course, and suggests the full URL
including the `.html` suffix. But that does not look as nice, and makes
it actively harder to copy/paste helpful, "pretty" links.

So let's just go ahead and strip off that unneeded file extension from
the search results' links.

Signed-off-by: Johannes Schindelin <johannes.schindelin@gmx.de>

static/js/application.js

@@ -263,6 +263,7 @@ var Search = {
                 result.data = await results.results[displayCount].data();
                 if (!i || typeof results.results[i - 1].data === 'object') categorizeResult(i);
                 result.data.meta.title = result.data.meta.title.replace(/^Git - (.*) Documentation$/, "$1")
+                result.data.url = result.data.url.replace(/\.html$/, '')
                 result.li.html(`<a href = "${result.data.url}">${result.data.meta.title}</a>`);
               })(displayCount).catch((err) => {
                 console.log(err);