On Wed, 16 Sep 2020 at 12:49, Jan Nieuwenhuizen <jann...@gnu.org> wrote:
> Meanwile we have a duplicate bug: <https://bugs.gnu.org/43435> > (it finally rang a bell on IRC...). I have closed the duplicate referencing this one. Sorry for missing this one. Cheers, simon