diff options
Diffstat (limited to 'scripts')
| -rwxr-xr-x | scripts/jenkins/release.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/jenkins/release.sh b/scripts/jenkins/release.sh index 8c1e46bc..bb512f70 100755 --- a/scripts/jenkins/release.sh +++ b/scripts/jenkins/release.sh @@ -23,7 +23,7 @@ ARG_DEFS=( ) function init { - if [[ $(git rev-parse --short HEAD) != $COMMIT_SHA ]]; then + if [[ $(git rev-parse HEAD) != $(git rev-parse $COMMIT_SHA) ]]; then echo "HEAD is not at $COMMIT_SHA" usage fi |