Make the formatting script ignore the three files that are formatted differently on different machines using the same clan-format version