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?
Experimentally iterate until something workable comes about. This way it's done publicly and people can collaborate.
