From e3846dbba0af464c32154cfaee7c302c799e6e0f Mon Sep 17 00:00:00 2001 From: Andrea Mazzoleni Date: Wed, 29 Oct 2025 14:47:17 +0100 Subject: [PATCH] Add fast check script --- makecheck.sh | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100755 makecheck.sh 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