configure: more properly disable header when check_header_oc() fails

This should make no difference currently Signed-off-by: Michael Niedermayer <michaelni@gmx.at>
2014-04-05 13:29:28 +02:00 · 2014-04-05 13:29:28 +02:00 · 323c049c7e
parent 7d2116dd09
commit 323c049c7e
1 changed files with 1 additions and 0 deletions
--- a/1
+++ b/1
@ -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; }"