> -----Original Message----- > From: Johannes Schlüter [mailto:johan...@php.net] > Sent: Friday, October 14, 2016 12:37 AM > To: PHP internals list <internals@lists.php.net> > Cc: Davey Shafik <da...@php.net>; Anatol Belski <anatol....@belski.net> > Subject: [PHP-DEV] IMPORTANT: Git reset after wrong merge > > Hi, > > as Davey noted in the thread "Master merged into PHP-7.1" there was a wrong > merge in git. This wasn't noticed for a few days. This means we had a few > additional commits in between. > > I've reseted PHP-7.1 to the *old* state *before* that merge. Quite a few > commits have been removed and need to be applied again (I hope Davey / > Anatol look after this) > > A backup of the bad tree is on > https://github.com/johannes/php-src/tree/broken-5.7-20161014 > > When pushing please be careful that you are not pushing master again into PHP- > 7.1. Please check your local trees carefully, commit > bce17764be6bd5ca43a512db51c030fb8d0437fd should NOT be in 7.1! > Yeah, we'll be checking to restore the missing 7.1 commits. Currently merges 7.0 to 7.1, or 7.1 to master, might have issues. I'd ask to please retain from pushing there, until the branch is restored. Hopefully this will happen at some point tomorrow.
Thanks Anatol -- PHP Internals - PHP Runtime Development Mailing List To unsubscribe, visit: http://www.php.net/unsub.php
