On Wed, Oct 17, 2018 at 06:24:42PM +0200, Ludovic Courtès wrote:
> LGTM, thanks!

Thanks! Pushed as 7277d06d8b956263ef1773c5f61e53dc65583ddd