diff --git a/configure b/configure index 95b44e7900..85de53ca63 100755 --- a/configure +++ b/configure @@ -7497,6 +7497,20 @@ cat <