On 15.08.2013 19:55, Johannes Schlüter wrote:
> Important: To ensure you don't push them by accident please run this
> command to delete them from your local clone:
>
> $ git branch -d 5.3 5.4 5.5
> Deleted branch 5.3 (was 15b554c).
> Deleted branch 5.4 (was bcdac75).
> Deleted branch 5.5 (was 4c76215).
And to ensure you never push garbage by accident, run this to tell git
to always only push the branch you're on when you run `git push`:
git config --global push.default current
Cheers
--
Jordi Boggiano
@seldaek - http://nelm.io/jordi
--
PHP Internals - PHP Runtime Development Mailing List
To unsubscribe, visit: http://www.php.net/unsub.php
