Heh, I didn't expect to get much attention for this. I thought it would be funny to push a merge commit between the 2 repo's latest commits. As a result, the git history is accessible from the dmca repo if you know the commit hashes. Since I didn't rebase, all the commit hashes were preserved with signatures. Another fun discovery is that deleting my fork of github/dmca didn't affect the PR like I thought it would, s…
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.
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.