Opened 20 months ago

Last modified 20 months ago

#29549 new task

How can we close obsolete GitHub pull requests?

Reported by: teor Owned by:
Priority: Medium Milestone: Tor: unspecified
Component: Core Tor/Tor Version:
Severity: Normal Keywords: tor-github
Cc: Actual Points:
Parent ID: Points: 1
Reviewer: Sponsor:


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:

Child Tickets

Change History (1)

comment:1 Changed 20 months ago by nickm

Current practice: I try to remember to close pull requests when I merge some different variant of them (e.g. cherry-picked or rebased). But sometimes I forget. Once in a while, I have been going through the pull requests and closing the merged ones manually -- but I haven't done that in a couple of months, I think.

Note: See TracTickets for help on using tickets.