diff --git a/tools/configure b/tools/configure index d8eef9f0af..3814d7583a 100755 --- a/tools/configure +++ b/tools/configure @@ -739,22 +739,22 @@ cat <