I just realized the existence of the web page https://www.tug.org/texdoc/ and mailing list https://lists.tug.org/texdoc I will hence post this issue there instead of the present list. Sorry for the noise. Bruno Voisin