March 18, 2022
11:20 p.m.
On 3/17/22 11:05, Matt Johnson-Pint wrote:
Regarding pull requests, you might consider setting up this GitHub Action: https://github.com/marketplace/actions/repo-lockdown
That would require changing the development repository to have files specific to GitHub, right? Other things being equal, it's better to stay portable and not rely on or promote GitHub-specific features. If the GitHub problem were a serious one it would be worth changing the development repository even in a nonportable way; however, this problem seems relatively minor.