Files here are generated from make_phpdoc_docs.sh