On 7/12/2014 1:38 PM, Johannes Pfau wrote:
But you've got some nice bonus: If somebody doesn't like your pull request you can just merge it anyway.
I'd only do that in an emergency. I'll also just pull the ones for D1.
But if you veto something the only one who can probably merge anyway is Andrei.
Andrei and I don't always agree, but we've not gone around overriding each other.