Give the `main` page a non-empty title in the TOC.
The intent is that we'll roll that page over to a release specific
page when we cut a release and then empty out `main` again.
Enable the magiclink extension for mkdocs, so that GH issue number
links work without any additional ceremony.
Rather than using `bash` for the mix of shell and output,
use `console`. That will cause the text to be marked up so
that the `$` prompt stuff won't get selected by dragging.
Enable copy button to copy the whole block, and add some
js to filter out the the $ and # prefixes from that content.
Ideally there would be a good mkdocs based checker, but the
one that is out there only validate absolute URLs, which makes
it unsuitable for checking local relative links in the docs.
Adjust the doc build so that we also generate the SUMMARY.md
for mdbook, and use mdbook's link checker to check the links.
Fixup the couple of broken links that it found.
Previously, I was cleaning up some junk like _index directories
generated from the _index.md fragments. I noticed that those
were showing up in the search index, so it is better to exclude
from the outset. mkdocs doesn't natively support the idea of
exclusion, but there is a plugin that does, so use it.
Remove a redundant parent node to simplify things.
A couple of Page entries were just containers and
had no content of their own; you can now set the filename
to None to indicate that, and adjust what gets emitted
in the nav.