diff --git a/configure b/configure index 1098fe66dba9a2c839d40a12b71b2ae6b915031d..5ca69c4241bf1b278fe8723385207d564ee8cbfa 100755 --- a/configure +++ b/configure @@ -947,6 +947,7 @@ check_header_oc(){ log check_header_oc "$@" header=$1 shift + disable_safe $header { echo "#include <$header>" echo "int main(void) { return 0; }"