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