Hello Michael,
On Mon, Jul 26, 2021 at 01:28:17AM +0200, Michael Kerrisk (man-pages) wrote:
> you reported this bug in July 2020, and i fixed it already then.

Apologies again, same double failure. FIXME is now gone.

Greetings

          Helge
-- 
      Dr. Helge Kreutzmann                     debian@helgefjell.de
           Dipl.-Phys.                   http://www.helgefjell.de/debian.php
        64bit GNU powered                     gpg signed mail preferred
           Help keep free software "libre": http://www.ffii.de/