diff --git a/tools/configure b/tools/configure index e674e557a3..1857e65483 100755 --- a/tools/configure +++ b/tools/configure @@ -1810,9 +1810,9 @@ cat <