diff --git a/tools/ci.sh b/tools/ci.sh index 26def3cc4d..3e34bd6fa8 100755 --- a/tools/ci.sh +++ b/tools/ci.sh @@ -1011,6 +1011,7 @@ function _ci_main { _ci_help ;; (*) + set -e cd $(dirname "$0")/.. while [ $# -ne 0 ]; do ci_$1