Hi,

On 8 December 2023 06:46:50 GMT+08:00, "Ludovic Courtès" <ludovic.courtes@inria.fr> wrote:

>Five years later, it seems reasonable to drop the patch (which is likely
>untested these days).  If you disagree, now’s the time to make your
>voice heard!