Anthony Ettinger
Admin
Our PR sweep kept trying to repair PRs that were already merged, asking GitHub to update a branch the merge had just deleted. Fix: only repair open PRs, and stop polling mergeability on closed ones. Also 8s faster per merged PR.