#5743 reminded me:

We still use an ancientmake.py that is based on what early versions ofsphinx-quickstart used to generate. We should probably modernize this to use a Makefile like current versions of sphinx create.

This is sort of low-priority, because the onlyreal advantage would be consistency with other Python projects. The Makefile won't magically make things faster or anything. Also, the work is non-trivial since ourmake.py includes customizations and other things that get run that will need to be ported to the "current way to do things" (probably Sphinx extensions).