Index: headers.awk
==================================================================
--- headers.awk
+++ headers.awk
@@ -3,13 +3,15 @@
 
 	gsub(/^"/, "", file);
 	gsub(/"$/, "", file);
 
 	destfile = file;
-	if (!gsub(/^.*\/include\//, "", destfile)) {
-		if (!gsub(/^.*\/include-fixed\//, "fix/", destfile)) {
-			next
+	if (!gsub(/^.*\/gcc\/.*\/include\//, "gcc/", destfile)) {
+		if (!gsub(/^.*\/include\//, "", destfile)) {
+			if (!gsub(/^.*\/include-fixed\//, "fix/", destfile)) {
+				next
+			}
 		}
 	}
 
 	if (file ~ /</) {
 		next;