Dmitriy, Yes, I agree that it is a totally great feature! But I would like to be sure that it does no harm.
BTW, I use a copy of git repo on my machine to deal with merges without touching my working tree. чт, 6 июн. 2019 г. в 19:21, Dmitriy Pavlov <dpav...@apache.org>: > > Hi Ivan, Igniters, > > Merge PRs via GitHub is the greatest change that Infra did recently. > > You can merge PRs without changing your local project state, and which is > why I believe is an absolutely positive thing for the community. Committers > can do a review-merge while waiting for tests run, doing a big feature > locally: any activity they have locally does not affect review now. > > Sincerely, > Dmitriy Pavlov > > чт, 6 июн. 2019 г. в 19:03, Павлухин Иван <vololo...@gmail.com>: > > > It seems that the majority of recent commits were made manually. If I > > am not mistaken there should be a badge with a green text "Verified" > > near a commit if it was made via GitHub web UI. And currently I see > > only a few such commits. > > > > чт, 6 июн. 2019 г. в 18:48, Petr Ivanov <mr.wei...@gmail.com>: > > > > > > 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 > > > > > > > > > -- > > Best regards, > > Ivan Pavlukhin > > -- Best regards, Ivan Pavlukhin
