On 6/2/16 5: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). 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.
Feel free to reopen if it helps, it wasn't closed in anger. -- Andrei
