On 06.12.2012, at 3:38, Sara Golemon <poll...@php.net> wrote: > RTFMing is hard, thanks. :) > > remote: Welcome pollita. > remote: Changesets accepted. Thank you for your contribution. > remote: > remote: Attempting to push to mirror g...@github.com:php/php-src.git > remote: Write failed: Broken pipe > remote: fatal: The remote end hung up unexpectedly > To https://git.php.net/push/php-src.git > c058ed5..5ac3577 master -> master > > The push to git.php.net succeeded, but its push to github failed. Is > there a process that deals with keeping the repos in sync in events > like this?
I believe it will eventually sync, as "push" propagates all changes, not just specific commit -- PHP Internals - PHP Runtime Development Mailing List To unsubscribe, visit: http://www.php.net/unsub.php
