Sorry about the churn on stan-dev/stan


#1

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.


#2

I’m surprised I haven’t done this yet haha. Praise be to git for making these things fixable.


#3

Might want to check that owners are disallowed


#4

There aren’t any additional check boxes that I have control over.


#5

I did this once, too, and it really surprised me.

Does the protection need to be on the client side?


#6

@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.


#7

This is not on Stan but on another repo I manage.


#8

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