t.texi:1: Seuls @fonttextsize 10 ou 11 sont autorisés, pas « 42 »