On 6/2/2016 2:05 PM, tsbockman wrote:
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).
I've done that, but that doesn't apply here.
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.
That doesn't seem to apply here, either.
Either way, they shouldn't be closed just because they say "do not merge"
(unless they're abandoned or something, obviously).
Something like that could not be merged until 132 other PRs are done to fix
Phobos. It doesn't belong as a PR.
