bail out on unknown PHP version

diff --git a/Makefile b/Makefile
index d20e6a420344dd344d47b76f844227aabb84ab6e..e0e3a6b836f7e20b9a5d9fa07c74e5eb4b618f99 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -75,6 +75,7 @@ clean:
 .PHONY: check
 check: $(PHP_RELEASES)
        @if test -z "$(PHP)"; then echo "No php version specified, e.g. PHP=5.6"; exit 1; fi
+       @if test -z "$(PHP_VERSION)"; then echo "No PHP version akin to $(PHP) available"; exit 1; fi
        if test -d $(srcdir)/php-$(PHP_VERSION)/.git; then cd $(srcdir)/php-$(PHP_VERSION)/; git pull; fi
 
 .PHONY: reconf