On Tue, Feb 19, 2019 at 08:52:08AM +0100, Ricardo Wurmus wrote:
> Feel free to push your patches.  Thanks!

I added some more comments and links to bug reports and pushed as
a7db61a55dc4e369574e206a86f9e5721f4a890b.

Thanks for your review, Ricardo!