diff --git a/tools/configure b/tools/configure index aaed8a4029..437a70bb2f 100755 --- a/tools/configure +++ b/tools/configure @@ -1310,29 +1310,31 @@ cat <