1/phpext_/ { 2 if (old_filename != FILENAME) { 3 printf "#include \"" FILENAME "\"@NEWLINE@" 4 old_filename = FILENAME 5 } 6} 7