This PR removes the sphinx.ext.githubpages extension from the Sphinx configuration file. That extension supplies a .nojekyll file, that's useless in practice because of the way we're managing docs in this repository - we only need a single .nojekyll file at the root of the repository.
This PR removes the
sphinx.ext.githubpagesextension from the Sphinx configuration file. That extension supplies a.nojekyllfile, that's useless in practice because of the way we're managing docs in this repository - we only need a single.nojekyllfile at the root of the repository.