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

[Eli Zaretskii]

> From: Lars Ingebrigtsen <address@hidden>
> Cc: Dmitry Gutov <address@hidden>,  address@hidden,  address@hidden,
>   address@hidden
> Date: Wed, 20 Nov 2019 12:15:18 +0100
> 
> Eli Zaretskii <address@hidden> writes:
> 
> > If we want to support pull requests, there are more things to do than
> > just the above.
> 
> I don't think our work flow has to change for pull requests.

Not our work, the setup for the server that will host the repositories
to which users push their changes for pull requests.

> 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.