The CVS-style $Id$ lines are pretty much useless with git; and
anyway, using them would require adding proper "ident" directives
to the .gitattributes file -- and we don't have such directives.

This change removes some occurrences of $Id$ lines that have been
missed by yesterday's commit 44745e29.