The make_distrib script will now generate Doxygen docs by default if the doxygen command-line tool is installed. Run with `--no-docs` (`--no-distrib-docs` with automate-git.py) to disable docs generation.
Marshall Greenblatt