diff --git a/tools/configure b/tools/configure index 328c54845e..9390fa1bf9 100755 --- a/tools/configure +++ b/tools/configure @@ -1331,7 +1331,7 @@ cat <