If it was really GitHub problem — it is still single incident among many tens of merges every day. Manual merge after review would more erroneous I guess.
> On 6 Jun 2019, at 18:43, Павлухин Иван <vololo...@gmail.com> wrote: > > Hi Igniters, > > I find merging PRs using GitHub web UI quite handy. AFAIK it is > possible to merge AI PR in this way. But I heard some rumors that > there were some problems with squashing such merges leading to commits > with multiple parents in master > > From recent there is one commit [1] but I am not sure that GitHub > merge caused it. > > So, my general question is as follows. Should we merge PRs via GitHub > web UI or should we avoid it? > > [1] > https://github.com/apache/ignite/commit/22652aa9883cfa3fd020658bcb230cea9ea6e4d4 > > -- > Best regards, > Ivan Pavlukhin
