diff --git a/tools/configure b/tools/configure index 16370b6cc0..e4ed05884a 100755 --- a/tools/configure +++ b/tools/configure @@ -1645,40 +1645,40 @@ cat <