Merge pull request #1234 from DimitriPapadopoulos/pedantic Pedantic suggestions GitOrigin-RevId: 9c08358277c62abbaee16b5ae138de98b218b248 Change-Id: I4b06e95c342f817ab43e8ab15ee8437f03ed3c15