diff --git a/tools/configure b/tools/configure index 307f66aa70..f60b4bfc16 100755 --- a/tools/configure +++ b/tools/configure @@ -72,6 +72,13 @@ EOF echo "Created Makefile" } +if [ "$target" = "--help" -o \ + "$target" = "-h" ]; then + echo "Just invoke the script and answer the questions." + echo "This script will write a Makefile for you" + exit +fi + # get our current directory pwd=`pwd`;