On Sun, Sep 8, 2024 at 3:24 AM Dmitry Gutov <dmi...@gutov.dev> wrote: > > On 07/09/2024 10:20, Eli Zaretskii wrote: > > Ping! Is this issue resolved and can be closed, or do we need to do > > anything else here? > > I suggest installing the following. Not a hard necessity, but seems like > an improvement:
Let's not, for all the reasons enunciated up-thread. João
