Re: "If you're still seeing problems, please reopen." [Was: bug#25148:]

[Eli Zaretskii]

> From: João Távora <address@hidden>
> Date: Wed, 20 Nov 2019 16:53:09 +0000
> Cc: Lars Ingebrigtsen <address@hidden>, Óscar Fuentes <address@hidden>, 
>       emacs-devel <address@hidden>, Richard Stallman <address@hidden>, Dmitry 
> Gutov <address@hidden>
> 
> On Wed, Nov 20, 2019 at 4:27 PM Eli Zaretskii <address@hidden> wrote:
> 
> > > Of course, if somebody wants to hit the "merge pull request" button
> > > in Gitlab, they can do that, but for most smaller pull requests,
> > > Gitlab would just email the patch (presumably) and we can apply it
> > > locally on our machines before pushing to the repo, just like now.
> >
> > What you describe is not the PR workflow that people are used to.
> 
> I don't think it's very far off, though.  Here's my usual workflow with
> GitHub, in the hope that it helps the discussion:

AFAIU, you described the wokflow of a developer, not of a
contributor.  I was rather talking about the latter, and mainly before
their PR is accepted and merged.