[PHP-DEV] Documenation bugs

[jeroen]

Hm, it now seems dat documenation bugs ONLY go to phpdoc, and NOT to php-dev anymore (see#11650). And the update went ONLY to php-dev... I don't know whether this is just coincidence, or it is broken now...   Greetz, Jeroen