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