I accidentally pushed a commit to Stan’s develop branch directly. I didn’t know I had the power to do so (we have branch protection turned on). I just removed the commit and we’re back to where we were before I did that.
Just FYI, the change was updating the math library to a branch (I’m working on the build branch). It was never meant to be merged directly.
Anyway, things are back to normal now.
I’m surprised I haven’t done this yet haha. Praise be to git for making these things fixable.
Might want to check that owners are disallowed
There aren’t any additional check boxes that I have control over.
I did this once, too, and it really surprised me.
Does the protection need to be on the client side?
@syclik: when I click on the “edit” button next to a protected branch, I see a checkbox in the next page that says “include administrators”. I think that should protect from this issue.
This is not on Stan but on another repo I manage.
I found the checkbox. Thanks for cluing me in on that!