Merge branch 'master' of git://factorcode.org/git/factor

db4
Slava Pestov 2008-11-11 10:51:34 -06:00
commit 7bb9e8d3ce
1 changed files with 16 additions and 4 deletions

View File

@ -339,7 +339,19 @@ cd_factor() {
check_ret cd
}
check_makefile_exists() {
if [[ ! -e "Makefile" ]] ; then
echo ""
echo "***Makefile not found***"
echo "You are likely in the wrong directory."
echo "Run this script from your factor directory:"
echo " ./build-support/factor.sh"
exit 6
fi
}
invoke_make() {
check_makefile_exists
$MAKE $MAKE_OPTS $*
check_ret $MAKE
}