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