I see that diff on github but it is not places at core. Maybe the reason was that the push was hanging during transmission.
It seems the commit was pushed without going to code-review - this was possible because of a misconfiguration. Now direct pushes are blocked again, which means you would have gotten an error instead of an unclear situation.