On 2012-12-05, Sara Golemon <poll...@php.net> wrote: > 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?
No, the next push will sync it again. I can setup a cronjob to do that every 15mins. -- PHP Internals - PHP Runtime Development Mailing List To unsubscribe, visit: http://www.php.net/unsub.php
