How can we close obsolete GitHub pull requests?
Most of our GitHub pull requests are automatically closed when the commits in the pull request are merged.
But if we don't merge the exact commits from a pull request, it sticks around.
Here are some things we could do:
- Ignore old pull requests
- Close all pull requests older than N months
- Work out some clever way to identify obsolete pull requests, and automatically close them
We talked about this issue in Brussels: https://trac.torproject.org/projects/tor/wiki/org/meetings/2019BrusselsNetworkTeam/Notes/StableMaintainer#CurrentProcess
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information