A PR was apparently closed by renaming of the base branch. This may have been compounded by the fact that the commit to merge from a different repo has been deleted. I have managed to recreate the original commit (same SHA and everything) in the other repo and pushed it, but don’t see a way to re-open the PR, which I would have guessed could be done by changing the base branch selected. That option is not available. Any suggestions appreciated.
I assume this is why you can’t reopen the PR.
You should be able to create a new PR from the branch where you have the restored commit. Maybe link the old PR, if you want to preserve the connection?
Yeah, that is always a backup. I guess the question is how flexible the github system is. You can apparently reopen a PR that was closed by a forced push. Maybe this case is too far outside of what is typical. Thanks.