mirror of
https://github.com/php/doc-en.git
synced 2026-03-24 07:42:10 +01:00
This reverts commit 6a05d92a32.
On the request of Máté to fix the build.
It might make sense to rewrite history and force push to prevent revcheck issues, but that's another debate.