check that the makefile exists and stop if it doesnt

db4
Doug Coleman 2008-11-11 10:19:42 -06:00
parent f04b32ea02
commit 2c4e3ce9dc
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
}