We want to use the mkdocs-exclude plugin, which lets us exclude
particular files from the output directory. But plugins aren't
available in the debian-stable version of mkdocs, so ensure that we're
running a sufficiently new version. If we aren't, gracefully just skip
building the documentation.
