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