diff --git a/makecheck.sh b/makecheck.sh index ca4bcd7a..918f46a9 100755 --- a/makecheck.sh +++ b/makecheck.sh @@ -9,10 +9,10 @@ SOURCE=`pwd` # Dest directory DEST=`mktemp -d` -cd $DEST - make distclean +cd $DEST + if ! $SOURCE/configure; then exit 1 fi diff --git a/makesan.sh b/makesan.sh index d2686538..7a3efad8 100755 --- a/makesan.sh +++ b/makesan.sh @@ -60,8 +60,3 @@ if ! make check distclean; then fi cd $SOURCE - -if ! ./configure; then - exit 1 -fi - diff --git a/maketest.sh b/maketest.sh index 7c4d7bab..3adc7f63 100755 --- a/maketest.sh +++ b/maketest.sh @@ -58,8 +58,3 @@ if ! make check distclean; then fi cd $SOURCE - -if ! ./configure; then - exit 1 -fi -