Rebonjour,
Du côté de la Lumière ("Linux"), je plaisante :P, il y a une curiosité !
La zone d'ombre est que dans « Configuration -> Apparence des applications -> Styles et Polices GTK+ -> Polices GTK+ -> Utiliser une autre police », le changement du style de la police de caractère à un effet sur mes menus de l'IDE d'Arduino, mais que le changement de taille des caractères reste minuscule (aucun changement de taille), même si je mais la taille à 72 ou à 128 !?!
Bizarre bizarre !
L'ami René