From d07d3cf5ebe151d4c3a639d66a340f73ef7e028f Mon Sep 17 00:00:00 2001 From: Andreas Lauser Date: Wed, 9 Jan 2019 14:29:58 +0100 Subject: [PATCH] add a pre build check to ensure that the Evaluation code is identical with the one produced by the code generator --- jenkins/pre-build.sh | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100755 jenkins/pre-build.sh diff --git a/jenkins/pre-build.sh b/jenkins/pre-build.sh new file mode 100755 index 000000000..0c7173e2d --- /dev/null +++ b/jenkins/pre-build.sh @@ -0,0 +1,12 @@ +#! /bin/bash + +./bin/genEvalSpecializations.py + +if test -n "$(git diff)"; then + echo "The generated source files have been manually edited or the " + echo "code generator has been modified but not been run before " + echo "proposing the branch for merging." + exit 1 +else + exit 0 +fi