From ad5bbc408637cffd4cc2ba990abef529cf5fa6a3 Mon Sep 17 00:00:00 2001 From: Diego Biurrun Date: Sun, 1 Apr 2018 22:13:55 +0200 Subject: [PATCH] configure: Rename require_header() --> require_headers() This renaming was overlooked in the previous check_header() rename. --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/configure b/configure index 848fe4881f..f5e7f1578c 100755 --- a/configure +++ b/configure @@ -1184,8 +1184,8 @@ require_cc(){ check_cc "$@" || die "ERROR: $name failed" } -require_header(){ - log require_header "$@" +require_headers(){ + log require_headers "$@" headers="$1" check_headers "$@" || die "ERROR: $headers not found" }