What is closing these PRs, and why?

Core Workflow
1

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

2

Seems the author removed his repository.

3

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

4

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!

5

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
6

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.)