xref: /PHP-7.2/build/print_include.awk (revision 8d5af8cb)

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