On Tue, Feb 18, 2020 at 8:06 AM Kyotaro Horiguchi <horikyota(dot)ntt(at)gmail(dot)com>
wrote:
>
> The attached fixes that.
After commit 9573384 this patch no longer applies, but with a trivial
rebase it fixes the issue.
Regards,
Juan José Santamaría Flecha