On Thursday, 2 June 2016 at 22:20:49 UTC, Walter Bright wrote:
On 6/2/2016 2:05 PM, tsbockman wrote:
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.
I was just responding to the general question you posed about "do
not merge" PRs, not really arguing for that one, in particular,
to be re-opened. I'm sure @wilzbach is willing to explain if
anyone cares to ask him why he did it as a PR, though.
