On Tue, Oct 01, 2019 at 03:47:17PM +0200, Baptiste wrote:
> This patch fixes the issue reported by David in github issue 227.
(...)

Merged, thank you Baptiste! (and David for his synthetic observation
that unblocked the situation)

Willy

Reply via email to