'Retrieve deleted pull request on github?

I'm overseeing a small open source project and we use github. A contributor sent us a PR with some good work we really want to have, and would struggle to replicate, including some files that aren't code

Direct link if it's helpful: https://github.com/DS-13-Dev-Team/DS13/pull/1994

Unfortunately, this contributor got into a fight with another team member, things got out of hand, and he left the project, before I got around to reviewing and merging this work. He deleted his repo and closed the PR too.

We would still like to merge this contribution. He's given me verbal permission to do so, but has no interest in active participation anymore. Getting the files from him directly seems unlikely.

Is there any way for us to restore and reopen this pull request?

branchpull-requestrepo


Solution 1:[1]

Is there any way for us to restore and reopen this pull request?

You can at least check out hos PR branch locally

git fetch origin pull/ID/head:BRANCHNAME
git switch BRANCHNAME

(Rename BRANCHNAME with a local branch name which makes sense in your case)

From there you can:

  • push BRANCHNAME to your repository
  • open a new PR from there.

Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source
Solution 1

Related Questions