summaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorMichael Niedermayer <michaelni@gmx.at>2014-04-05 13:29:28 +0200
committerMichael Niedermayer <michaelni@gmx.at>2014-04-05 13:29:28 +0200
commit323c049c7e43cb610e3c5ffbe09fc46278808ad5 (patch)
tree98f9d52fba474384c5dbe8fb3a8b181618b6ae65 /configure
parent7d2116dd09d19d9aa08f9155a932d684c8d6a2f7 (diff)
configure: more properly disable header when check_header_oc() fails
This should make no difference currently Signed-off-by: Michael Niedermayer <michaelni@gmx.at>
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure1
1 files changed, 1 insertions, 0 deletions
diff --git a/configure b/configure
index 1098fe66db..5ca69c4241 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; }"