Hi Internals,
the Git migration is not finished yet and won't be finished for the
next weeks but we are constantly working on improvements.
There is now a new PHP Mailinglist called git-pulls@lists.php.net.
All pull requests requests created for the github.com/php user will
go to this mailinglist.
If you have commit rights to a mirrored PHP repository you can
pull the requests and push it to the official repositories. But please
note the following restrictions:
(1) You cannot use the Merge button on github for that. The PHP
Organization on PHP will not accept contributors. It's only
for mirroring!
(2) Pull the request (e.g. PR 23) using
$ git fetch git://github.com/php/web-php pull/23/head:pull-request/23
$ git log -p pull-request/23 # REVIEW IT
$ git merge pull-request/23 # Merge it, add a GOOD commit message
$ make test # you better don't forget that
$ git push origin master # everything okay? good, let's push it
(3) The pull reuqest will be automtaically closed. Closing a pull request
without merging is not possible as this is restricted to PHP organization
member. Due to the nature of our setup we cannot invite people to
that organization. If only one guy accidentally hits the Merge button
the whole setup is screwed.
dsp out