When building the docs with an old sphinx (like e.g. on Debian), this
would break links in the search results.
This happens because we've nabbed the searchtools.js from a sphinx to
add our special handling of short builtins like "and", "end", "cd" (as
part of #7757).
I don't believe this will change *a lot* in practice, so it's probably
still okay, but this hack is still worthwhile.
See #7946
Unfortunately this has both stopwords and a length limit, and things
like "and" just are tough to search.
So what we do is leave everything as it is, but when a search fails,
we show a list of things that are hard to search for, currently that's
"and", "for", "if" and such.
Fixes#7757.
