[tor-bugs] #29549 [Core Tor/Tor]: How can we close obsolete GitHub pull requests?

[Tor Bug Tracker & Wiki]

#29549: How can we close obsolete GitHub pull requests?
--------------------------+----------------------------------
 Reporter:  teor          |          Owner:  (none)
     Type:  task          |         Status:  new
 Priority:  Medium        |      Milestone:  Tor: unspecified
Component:  Core Tor/Tor  |        Version:
 Severity:  Normal        |     Resolution:
 Keywords:  tor-github    |  Actual Points:
Parent ID:                |         Points:  1
 Reviewer:                |        Sponsor:
--------------------------+----------------------------------

Comment (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.

--
Ticket URL: <https://trac.torproject.org/projects/tor/ticket/29549#comment:1>
Tor Bug Tracker & Wiki <https://trac.torproject.org/>
The Tor Project: anonymity online