/phpext_/ {
if (old_filename != FILENAME) {
printf "#include \"" FILENAME "\"@NEWLINE@"
old_filename = FILENAME
}