What is closing these PRs, and why?

Shouldn’t the closing be attributed to something, ideally with a message explaining why?

Seems the author removed his repository.

But the commit is still there in the pull request, why does it need the forked repo to keep the PR open?

I believe GitHub creates copies of PRs, so the original forks can be safely deleted and the PRs preserved.

So these PRs can be re-opened. The strange thing is these both say:

This pull request was closed.

Rather than saying who closed them (like the author, another user, or a bot, (for example)):

[user] closed this [time] ago.

@yiannis-had To clear up the mystery and help understand how GitHub works better :slight_smile: did you close the PRs before or after deleting your fork? Or did GitHub close them automatically? Thanks!

Hi, I had nothing to do with closing the PR, I guess it was done automatically.

I have been deleting forks after opening PRs in other repositories but never had this happen. For example, see: assert on replace_separators to enforce a string by yiannis-had · Pull Request #80 · amirziai/flatten · GitHub

1 Like

Thanks, that’s strange. I’ve asked about this on the GitHub discourse.

(In the meantime, I’ll re-open your PRs, and we can skip a news entry for for typos.)