Zulip Chat Archive

Stream: new members

Topic: Unmerged branch was closed

Paul Lezeau (Jan 11 2022 at 08:39):

My PR #9345 was dependent on PR #10941, which just got merged. The problem is that Bors also closed #9345, which hasn't been merged yet. Is there a way to reopen it, or should I just open a new PR?

Paul Lezeau (Jan 11 2022 at 08:43):

I think the issue is that I set #9345 to merge into the branch I was PR ing with #10941.

Yaël Dillies (Jan 11 2022 at 08:51):

Weird... seems like bors drank too much last night.

Eric Wieser (Jan 11 2022 at 08:51):

Fixed

Eric Wieser (Jan 11 2022 at 08:52):

I just undeleted the branch, reopened then changed the base of #9345, then redeleted the deleted branch. Your diagnosis is correct about why this happened

Eric Wieser (Jan 11 2022 at 08:53):

When a branch is deleted, Github automatically closes any PRs against that branch, and attributes the user who deleted the branch to their closure.

Paul Lezeau (Jan 11 2022 at 10:42):

Eric Wieser said:

Fixed

Great, thanks a lot!

Last updated: Dec 20 2023 at 11:08 UTC