diff --git a/tools/configure b/tools/configure index 5e562f58f5..0db6501288 100755 --- a/tools/configure +++ b/tools/configure @@ -1485,7 +1485,7 @@ cat <