diff --git a/CI/ci-linux.sh b/CI/ci-linux.sh index 30a08372..84455a33 100755 --- a/CI/ci-linux.sh +++ b/CI/ci-linux.sh @@ -3,6 +3,9 @@ COMPILER=$1 LANGUAGE=$2 +# Exit script on any error +set -e + OPTIONS="" if [ "$COMPILER" == "gcc" ]; then