1
0
mirror of https://github.com/php/php-src.git synced 2026-04-06 23:53:30 +02:00

Fail hard if sed isn't found

now that the new SDK is required and supplies it.
This commit is contained in:
Anatol Belski
2017-04-11 11:21:31 +02:00
parent be540347e2
commit fa7bd5eabf

View File

@@ -2880,7 +2880,9 @@ function toolset_setup_project_tools()
}
/* TODO throw error, ignore for now for BC. */
PATH_PROG('sed');
if (!PATH_PROG('sed')) {
ERROR('sed is required')
}
RE2C = PATH_PROG('re2c');
if (RE2C) {