PRs with deleted fork

[ashawley]

When a PR's fork is deleted by the fork's owner, the PR says the branch is "unknown repository". When querying the GitHub api about the open PRs, the branch repo info is unavailable (pr.head.repo is null). Admittedly, there's probably no way around this unfortuitous situation. It requires manual intervention to either merge the PR, or re-open the PR with the branch in an available repo. There's a chance that one could use the GitHub API find an alternate way to somehow find git refs to merge. However, what's unacceptable is the error message in this situation:

ERROR prs.Main$:230 - java.util.NoSuchElementException: None.get 

A more helpful error message could be "No repo information found for pull request: owner/project#123"

[ashawley]

Alternatively, there is a way to retrieve a pull request branch by the PR number.

https://help.github.com/en/articles/checking-out-pull-requests-locally