Remix.run Logo
mlugg 8 hours 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.

noname120 2 hours ago | parent | next [-]

You can close them and limit discussion to contributors I guess? Not ideal but at least they wouldn’t appear in the pull requests tab.

Alternatively you can use a bot or a GitHub Action to automatically change the description and title of the pull request to something like “[PRs are not allowed and deleted automatically]”. But yeah not a perfect solution either…

ACCount37 2 hours ago | parent | prev [-]

It's completely intentional, and goes back to when GitHub was founded. GitHub was intended as a collaborative software development platform, not "look but don't touch".

noname120 2 hours ago | parent [-]

I suppose you can fork a repository if you want to collaborate with others though. Reviewing pull requests and engaging with a community is a lot of work and has possible legal ramifications; in many cases it’s faster to just do things yourself. Some teams/companies deliberately refuse outside contributions for this reason.