On 2019-06-14 23:14:09 +0100, Andrew Gierth wrote: > So here is my current proposed fix.
Before pushing a commit that's controversial - and this clearly seems to somewhat be - it'd be good to give others a heads up that you intend to do so, so they can object. Rather than just pushing less than 24h later, without a warning. - Andres
