diff options
| -rwxr-xr-x | configure | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/configure b/configure index 3f823ed163..c20ed86ff3 100755 --- a/configure +++ b/configure @@ -1875,6 +1875,10 @@ if test -z "$python" then error_exit "Python not found. Use --python=/path/to/python" fi +if ! has "$make" +then + error_exit "GNU make ($make) not found" +fi # Note that if the Python conditional here evaluates True we will exit # with status 1 which is a shell 'false' value. |