Index: headers.awk
==================================================================
--- headers.awk
+++ headers.awk
@@ -2,11 +2,11 @@
 	file = $3;
 
 	gsub(/^"/, "", file);
 	gsub(/"$/, "", file);
 
-	while(gsub(/\/[^\/]*\/..\//, "/", file)) {}
+	while(gsub(/\/[^\/]*\/\.\.\//, "/", file)) {}
 
 	destfile = file;
 	if (!gsub(/^.*\/gcc\/.*\/include\//, "gcc/", destfile)) {
 		if (!gsub(/^.*\/include\//, "", destfile)) {
 			if (!gsub(/^.*\/include-fixed\//, "fix/", destfile)) {