On Thursday, 2 June 2016 at 20:56:26 UTC, Walter Bright wrote:
What is supposed to be done with "do not merge" PRs other than close them?
Occasionally people need to try something on the auto tester (not sure if that's relevant to that particular PR, though). Presumably if someone marks their own PR as "do not merge", it means they're planning to either close it themselves after it has served its purpose, or they plan to fix/finish it and then remove the "do not merge" label.
Either way, they shouldn't be closed just because they say "do not merge" (unless they're abandoned or something, obviously).
