diff --git a/tools/configure b/tools/configure index 11ff981fdb..5e562f58f5 100755 --- a/tools/configure +++ b/tools/configure @@ -1471,7 +1471,7 @@ cat <