Pull requests with 'DO NOT MERGE' label

Hi everybody,

There are 56 open pull requests with the ‘DO NOT MERGE’ label, with some going back to 2017. I’m sure some of these aren’t ever going to be merged or at least the pull request needs a lot of work before it would be merged. If you can take a look at them to close them or add comments as appropriate, that would be appreciated. Thanks!



FTR, here is a link to the list of these PRs.

Also, there are a further 19 PRs that match “WIP” but don’t have the DO-NOT-MERGE label.

I propose to simply close the oldest PRs, but with a friendly warning 1 month before.

Maybe send a warning that you will close a PR if there is no activity in one month, and one month later, close the PR. I suggest to do that on PR which are older than 1 year.

If the author wants to work again on the change, it’s easy. The branch is not closed: the PR can be reopened, or a new PR can be created. Maybe explain that when you close the issue.