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