On Wed, Sep 16, 2020 at 1:20 PM Matteo Beccati <p...@beccati.com> wrote:
> Hi Nikita, > > On 16/09/2020 12:46, Nikita Popov wrote: > > No, this just means that your CI is running tests that our CI doesn't. > > In this case, you are probably using a different MySQL version and thus > > run a different subset of tests. > > I know that, and that's why I keep it running it ;-) > > I was just saying that some commits aren't getting to the php-cvs > mailing list, and often that happens when closing GitHub PRs. And I > suspect it has somethinig to do with the way the PR merge is handled. > Oh sorry, completely misunderstood what you were referring to. I believe this is related to the size of the diff. Large diffs probably run into some size limit and don't reach the php-cvs list. Nikita
