diff --git a/dev/make-distrib.sh b/dev/make-distrib.sh index 2e599b39b4d5bfb943775afdc56502a7c3f7f68d..8d737c5cc40734719d52fd26373d4940b6cf6e8b 100755 --- a/dev/make-distrib.sh +++ b/dev/make-distrib.sh @@ -21,6 +21,8 @@ # # ########################################################################## +set -e + ################################################################################ # Configuration @@ -290,8 +292,7 @@ $HDRCK -update $MAKE_HEADER_OPT -spec-format="3-fields-by-line" -C "$TMP_DIR/$FR # Sanity check if [ "$OPEN_SOURCE" == "yes" ] ; then - OUT=$(grep -Iir "Contact CEA LIST for licensing." $TMP_DIR | grep -v "headers/" | grep -v "dev/make-distrib.sh") - if [ "$?" == "0" ]; then + if grep -Iir --exclude-dir="headers" --exclude="make-distrib.sh" "Contact CEA LIST for licensing." $TMP_DIR; then echo "Looks like there are some files containing undetected closed source licences" exit 1 fi