PR closed instead of merged

futurelearn / squiddy

Github Actions bot

1 stars 1 forks source link

PR closed instead of merged #13

Closed thomasmarshall closed 3 years ago

thomasmarshall commented 3 years ago

This PR appears "closed" rather than "merged" even though the commits have been successfully rebased and merged into the master branch.

It looks like the force-push event happened, but the commit hashes listed in the PR haven't updated. I wonder if GitHub couldn't recognise that the commits had been merged, maybe because the branch was deleted before GitHub had a chance to register the force-push event?

elenatanasoiu commented 3 years ago

This should be fixed by https://github.com/futurelearn/squiddy/pull/16

Closing for now. I'll re-open if it happens again.