I know, but I prefer `python make.py html` for the doc building itself, as this will only build the changed pages and a full doc build can really take quite a while. So for iteratively working on the docs, this is mostly preferred IMO. Only if you want a full build, you have to do something else, and then I thought it was easier to mention `python make.py clean` instead of `make doc` (yet another command + you need to be in another directory). Thoughts?