Simon Peyton Jones via ghc-devs
| You believe the one which marge posts telling you that the patch is | merged, the commit it links to is on master so you can clearly see the | patch has been committed.
OK. The earlier one, also from Marge, not the Discussion stream but rather in the panel at the top, says
Closed by Marge Bot 8 hours ago The changes were not merged into master
So that is an outright lie? Yes it is closed, but contrary to the statement it _has_ been merged.
It's unfortunate that this misleading display is right at top, in the summary material, while the truth (that it has been merged) is buried in the Discussion stream.
Alas. But thank you for clarifying.
Is this something we can raise with the Gitlab folk? It seems so egregiously wrong.
Indeed this is a bit of a limitation of GitLab and is a result of the fact that our Marge fork uses a somewhat hacky workflow for its merges to work around other GitLab bugs. There is indeed GitLab issue [1] requesting the ability to manually mark merge requests as merged, but it seems unlikely that this will happen in the near future. Thankfully, our days of using Marge are numbered. GitLab 12.0, which shipped two weeks ago, introduced Merge Train support. I haven't yet upgraded our installation but will try to do so this week. There are a few annoying limitations of merge train support surrounding forks, but I believe we can work around these for the time being. Cheers, - Ben [1] https://gitlab.com/gitlab-org/gitlab-ee/issues/3033