diff --git a/configure b/configure index c95d900553..0cc53f893a 100755 --- a/configure +++ b/configure @@ -551,6 +551,23 @@ int main(void){ EOF } +check_type(){ + log check_type "$@" + headers=$1 + type=$2 + shift 2 + disable $type + incs="" + for hdr in $headers; do + incs="$incs +#include <$hdr>" + done + check_cc "$@" <