We generate documentation into the doc/ directory, so we shouldn't be
intermingling source files with generated files