[Tutti-commits] 01/01: modif du formatter de commentaires pour remplacer les points virgule par des points (fixes #7128)