diff --git a/tools/configure b/tools/configure index 7c9e3773c6..2b29a3d784 100755 --- a/tools/configure +++ b/tools/configure @@ -1535,65 +1535,60 @@ if [ "$ARG_TARGET" ]; then else echo "Enter target platform:" cat <