Oops, accidentally pushed to develop

Developers
1

I’m a moron. I just upgraded to boost 1.62 and wondered
why I didn’t get one of those create a pull request buttons
on the home page, then realized I’d forgotten to branch and
just pushed to develop.

It should be OK as it’s just a change to the Boost lib,
for which Ben had fixed compatibility in a previous pull
request.

Or if someone better than me wants to back it out and
turn it into a pull request, that’d work too.

Sorry about that.

  • Bob
2

This is the offending commit:

  • Bob
3

Lol. Do I need to take the keys away from you? (I thought we had the
permissions set up to not allow us to push directly, but I might have just
done that over stan. I’ll see if I can turn that permissions thing off.)

I’m just going to roll back develop to right before that commit. I can help
create a PR for Boost 1.62.

4

I don’t know how Discourse is counting:

changed 301 files with 0 additions and 19308 deletions.

Following the link to GitHub, I see:

13,905 changed files with 668,305 additions and 489,049 deletions.

  • Bob
5

I just set the branch back to before your commit. I’m going to make sure it’s protected properly. protected branches are a new feature in GitHub and I didn’t configure it correctly. In the future, you won’t be able to push directly.

6

Yes, I think so. It’d be great if it weren’t possible to
push directly to develop.

  • Bob
7

I think I correctly updated the settings so we shouldn’t be able to push
directly.

8

Thanks!

  • Bob
9

Want me to create a pull request?

10

Before GitHub allowed protected branches you had to set your local environment to prevent pushes to develop, so it was a fragile protection mechanism.