diff --git a/configure b/configure index 85549d12413d00cdce9132dd958b3b41f8bcb7b3..7fec59cb007368a4cdeec25a2402edc832ea439d 100755 --- a/configure +++ b/configure @@ -740,6 +740,16 @@ if test -z "$target_list" ; then exit 1 fi +feature_not_found() { + feature=$1 + + echo "ERROR" + echo "ERROR: User requested feature $feature" + echo "ERROR: configure was not able to found it" + echo "ERROR" + exit 1; +} + if test -z "$cross_prefix" ; then # ---