accidental push about repolinter

[willnorris]

cool, thanks for confirming.

[willnorris]

I'll try to poke through git reflog to see what the last commit master pointed to was, but it might be simpler for someoene else to look at your local check out to roll this back. @prototypicalpro can you take a look?

[willnorris]

reflog isn't much help. I can't easily tell how many commits I accidentally pushed us forward. It looks like the bulk of these changes were in the process of getting merged as part of #192 anyway, so maybe we just leave things as-is, complete the review, and fix anything that needs changing from there?

[willnorris]

Ah, looking at the slack message, it seems that 4cfa122 was the previous HEAD before this push. That would be the rollback point if we want to do that.

[prototypicalpro]

No worries! It looks like other than the PR there wasn't any other changes made, so it should be fine (that PR was about ready to me merged anyway). I double checked with a diff of my local copy and this repository and everything looks good, so I think I'm just going to leave it.