merging a pr

[tkellen]

if you delete a branch after merging a pr before hookshot can check it out, the deploy fails.

[cowboy]

Is it possible to use the branch's sha instead of its name? I'd imagine the commit would still persist, even if the branch was deleted (I could be wrong)

[brianloveswords]

I'd imagine the commit would still persist, even if the branch was deleted

My understanding of branches is that they are movable pointers to commits (opposed to tags, which are static pointers). My test in creating a new branch, making a commit, checking out master and deleting that branch shows that the commit remains:

Interestingly, I only tried for 5 minutes, but I can't figure out how to remove that now-orphaned commit. I tried git gc --aggressive and git remote prune origin (which is a useful command, but not what I was looking for) and neither got rid of it.

[cowboy]

It's possible that GitHub aggressively GCs no-longer-referenced blobs, but I dunno. Either way, if hookshot can use the sha of the branch in question, it might be less prone to failure.