top | item 46064980

(no title)

mlugg | 3 months ago

PRs are not optional: there is no way to disable them on GitHub. I can't be sure that this is intentional, but it certainly works out well for them that this is one of many properties which make it quite difficult to migrate away from the platform.

discuss

order

jamesnorden|3 months ago

There's technically a way[1], but you'd have to do it every 6 months which is not great.

https://docs.github.com/en/communities/moderating-comments-a...

mlugg|3 months ago

Yeah, that's actually what we've done on the Zig GitHub repository. However, it doesn't stop pushes to existing PRs, which isn't ideal; and, yes, it's quite hard to escape the conclusion that there being no "until I turn it back on" option is intentional.

chillfox|3 months ago

I guess you could make a bot that closes any opened PR with a message that PRs are not accepted on Github and a link to the contribution docs.