diff --git a/tools/configure b/tools/configure index 3dee5155db..7e70e21a3f 100755 --- a/tools/configure +++ b/tools/configure @@ -673,31 +673,31 @@ if [ "1" != `parse_args --target` ]; then else echo "Enter target platform:" cat <