diff --git a/tools/configure b/tools/configure index 7e70e21a3f..745c2ee7b8 100755 --- a/tools/configure +++ b/tools/configure @@ -683,7 +683,7 @@ cat <