Sorry about the churn on stan-dev/stan

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.

1 Like

I found the checkbox. Thanks for cluing me in on that!

1 Like