diff options
| -rwxr-xr-x | scripts/pre-push | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/scripts/pre-push b/scripts/pre-push index 945fb3519a..5d4e280d25 100755 --- a/scripts/pre-push +++ b/scripts/pre-push @@ -22,7 +22,9 @@ # <local ref> <local sha1> <remote ref> <remote sha1> # -RELEASES="21 20 19 18 17 r16 r15 r14 r13" +NEW_RELEASES="21 20 19 18 17" +OLD_RELEASES="r16 r15 r14 r13" +RELEASES="$NEW_RELEASES $OLD_RELEASES" # First commit on master, not allowed in other branches MASTER_ONLY=aea2a053e28a11497796879715be29ab0c3cd1a0 @@ -158,8 +160,24 @@ then exit 1 fi ;; - refs/tags/OTP-21.* | refs/tags/OTP-20.* | refs/tags/OTP-19.* | refs/tags/OTP-18.* | refs/tags/OTP-17.*) + refs/tags/OTP-*) tag=${remote_ref#refs/tags/} + REL="UNKNOWN" + for x in $NEW_RELEASES; do + if [ ${tag#OTP-$x.} != $tag ] + then + REL=$x + break + fi + done + if [ $REL = "UNKNOWN" ] + then + echo "$0 says:" + echo "***" + echo "*** Unknown OTP release number in tag '$tag'" + echo "***" + exit 1 + fi if [ "$remote_sha" != $null ] then echo "$0 says:" |