The patch looks good to me.
On Tue, Aug 11, 2020 at 9:42 PM Cyril Jouve <jv(dot)cyril(at)gmail(dot)com> wrote:
>>