Pull Request: https://github.com/php/web-php/pull/1100 Author: cmb69
Due to <https://github.com/php/doc-en/pull/3627>, the MongoDB documentation's main page has been moved; we redirect accordingly. --- Frankly, I have no idea where to put that redirect, or what would be the difference between `$manual_page_moves` and `$manual_redirections`. Maybe someone else knows.
