3 ms·
Would closing the PR be enough to remove it, or does it actually have to be deleted? I didn't think PRs could be deleted, only closed.
by JMTQp8lwXL 6y ago
Would closing the PR be enough to remove it, or does it actually have to be deleted? I didn't think PRs could be deleted, only closed.
- Stephen304 6y agoI don't think so, if you look at the other closed PRs, you can find some where the owner also deleted their fork like I did. Despite that you can still access the commits they wanted to merge.
- Arnavion 6y agoClosing will not be enough. Even deleting the fork that made the PR will not be enough. (The PR remains open and the commit URLs automatically get updated to point to the parent repo, just like the URL that was submitted.) Users can't delete PRs but GitHub can. They do it for PRs reported as spam, etc. Regardless, what's needed here is not just deleting the PR (and the fork) but also doing a GC (as Stephen304 said), which too is something only GitHub can do.