diff --git a/tools/configure b/tools/configure index 8b02d16dca..a2142d3264 100755 --- a/tools/configure +++ b/tools/configure @@ -723,8 +723,8 @@ cat <