diff options
-rwxr-xr-x | tools/configure | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/tools/configure b/tools/configure index 2dd1bf3e12..13cd5995b2 100755 --- a/tools/configure +++ b/tools/configure @@ -1287,7 +1287,7 @@ fi echo Using temporary directory $tmpdir if test -r "configure"; then - # this is a check for a configure script in the current directory, it there + # this is a check for a configure script in the current directory, if there # is one, try to figure out if it is this one! if { grep "^# Jukebox" configure >/dev/null 2>&1 ; } then @@ -1304,6 +1304,23 @@ if test -r "configure"; then fi fi +if test -r "tools/configure"; then + # this is a check for a configure script in the tools/ directory, if there + # is one, try to figure out if it is this one! + + if { grep "^# Jukebox" tools/configure >/dev/null 2>&1 ; } then + echo "WEEEEEEEEP. Don't run this configure script in the root of the tree." + echo "It will only cause you pain and grief. Instead do this:" + echo "" + echo " mkdir build-dir" + echo " cd build-dir" + echo " ../tools/configure" + echo "" + echo "Much happiness will arise from this. Enjoy" + exit 5 + fi +fi + # get our current directory pwd=`pwd`; |