Commit 2022-12-03 19:18 32e4a38c

fix(scripts/port_comments): deal with files that have no header to insert below (#17797) We want to insert the comment below the header, unless there is no header, in which case we just put it at the top. I'd assumed we didn't have any files without titles, but category theory is full of them! I've already successfully run this to add the most recent batch of comments.