https://gcc.gnu.org/bugzilla/show_bug.cgi?id=66136
--- Comment #8 from Szabolcs Nagy <nszabolcs at gmail dot com> --- the new awk version is supposed to produce the exact same output as the old script with gnu sed. the pasted output fragment looks ok.
