Closed lurch closed 1 year ago
ha i just got bitten by this myself :-)
I've just rebased this onto the latest develop
. (but I haven't re-tested it)
Should I re-open this against master
, or just leave it closed?
well reopen against develop
Ahhh, I saw the "kilograham deleted the branch raspberrypi:develop
yesterday" message (and I assume that is what auto-closed this PR?), but I didn't realise that you'd actually created a new develop
branch.
I don't have the permissions to re-open this PR, so I guess you could either do that for me, or I could create a fresh PR? (which would mean we'd lose your review-comments) - up to you.
BTW it's just occurred to me that if you made develop
a protected branch, then GitHub probably wouldn't try auto-deleting it each time you merge develop
into master
? :slightly_smiling_face: (and therefore any other PRs against develop
hopefully won't get auto-closed)
closing this - as the code s pretty stale... the verify option is a good workaround for this anyway, but feel free to re-open an issue