diff --git a/jenkins/quality.sh b/jenkins/quality.sh index 4cf26d76bf..56217af874 100755 --- a/jenkins/quality.sh +++ b/jenkins/quality.sh @@ -3,6 +3,8 @@ set -e set -x +git remote prune origin + # Reset the submodule, in case it changed git submodule foreach 'git reset --hard HEAD' diff --git a/jenkins/test.sh b/jenkins/test.sh index 8a96024785..7a61e914b7 100755 --- a/jenkins/test.sh +++ b/jenkins/test.sh @@ -15,6 +15,8 @@ function github_mark_failed_on_exit { trap '[ $? == "0" ] || github_status state:failure "failed"' EXIT } +git remote prune origin + github_mark_failed_on_exit github_status state:pending "is running"