diff --git a/makecheck.sh b/makecheck.sh new file mode 100755 index 00000000..ca4bcd7a --- /dev/null +++ b/makecheck.sh @@ -0,0 +1,22 @@ +#!/bin/sh +# +# Run a check in a temporary dir +# + +# Source directory +SOURCE=`pwd` + +# Dest directory +DEST=`mktemp -d` + +cd $DEST + +make distclean + +if ! $SOURCE/configure; then + exit 1 +fi + +if ! time make check; then + exit 1 +fi