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

[Eli Zaretskii]

> From: Lars Ingebrigtsen <address@hidden>
> Cc: address@hidden,  address@hidden,  address@hidden,  address@hidden
> Date: Thu, 21 Nov 2019 13:24:55 +0100
> 
> Eli Zaretskii <address@hidden> writes:
> 
> >> 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.
> 
> The first part of the sentence does, I think?

No, because before the contributor requests to merge, he/she must
submit the PR.  And that requires interaction with GitLab (or any
other service supporting PRs).