On Thu, Aug 03, 2017 at 12:10:00AM +0200, Ludovic Courtès wrote:
> Heya,
> 
> Leo Famulari <leo@famulari.name> skribis:
> 
> > Alright, pushed as 503c8c5882550005a7e9d3058a5f6d22f9c33f63. I'll keep
> > this bug open for a while to document further instances of this problem.
> 
> I think we’re mostly done with this bug, or am I optimistic?

Yes, I think so. We can always re-open if necessary :)