diff --git a/tools/configure b/tools/configure index d705c2f91b..d62f65f970 100755 --- a/tools/configure +++ b/tools/configure @@ -685,31 +685,26 @@ cat <