On 14.10.2016 at 04:25, Anatol Belski wrote:
> I would explicitly ask Dmitry, Sara, Hui, Stas, Bob, Nikita and
> Christoph to check that all the code pushed after Monday 2016-10-10
> 13:11:45 is where it's expected to be. But also everyone else
> involved/interested - it would be a big help to dou
Hi Yasuo,
> -Original Message-
> From: Yasuo Ohgaki [mailto:yohg...@ohgaki.net]
> Sent: Friday, October 14, 2016 4:08 AM
> To: Anatol Belski
> Cc: Johannes Schlüter ; PHP internals list
> ; Davey Shafik
> Subject: Re: [PHP-DEV] IMPORTANT: Git reset after wrong
> -Original Message-
> From: Anatol Belski [mailto:anatol@belski.net]
> Sent: Friday, October 14, 2016 1:11 AM
> To: 'Johannes Schlüter' ; 'PHP internals list'
>
> Cc: 'Davey Shafik'
> Subject: RE: [PHP-DEV] IMPORTANT: Git reset a
Hi Anatol,
On Fri, Oct 14, 2016 at 8:11 AM, Anatol Belski wrote:
> 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 hap
> -Original Message-
> From: Johannes Schlüter [mailto:johan...@php.net]
> Sent: Friday, October 14, 2016 12:37 AM
> To: PHP internals list
> Cc: Davey Shafik ; Anatol Belski
> Subject: [PHP-DEV] IMPORTANT: Git reset after wrong merge
>
> Hi,
>
> as Dav
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 b
