diff options
| author | Sverker Eriksson <[email protected]> | 2019-06-05 19:13:47 +0200 |
|---|---|---|
| committer | Sverker Eriksson <[email protected]> | 2019-06-05 19:46:02 +0200 |
| commit | fc1f0444e32b039194189af97fb3d5358a2b91e3 (patch) | |
| tree | 8b8cf7e77677fda75665b4ff8f2459836e2a109b /scripts | |
| parent | e4f73d4c214486691689857038c71c1093c84971 (diff) | |
| download | otp-fc1f0444e32b039194189af97fb3d5358a2b91e3.tar.gz otp-fc1f0444e32b039194189af97fb3d5358a2b91e3.tar.bz2 otp-fc1f0444e32b039194189af97fb3d5358a2b91e3.zip | |
Let pre-push hook detect when it needs an upgrade
after a master release.
Diffstat (limited to 'scripts')
| -rwxr-xr-x | scripts/pre-push | 27 |
1 files changed, 21 insertions, 6 deletions
diff --git a/scripts/pre-push b/scripts/pre-push index 670f1c9796..56a4eb945e 100755 --- a/scripts/pre-push +++ b/scripts/pre-push @@ -118,12 +118,27 @@ then fi if [ $remote_ref != refs/heads/master -a "$MASTER_ONLY" ] && git merge-base --is-ancestor $MASTER_ONLY $local_sha then - echo "$0 says:" - echo "***" - echo "*** INVALID MERGE: Commit $MASTER_ONLY should not be reachable from '$branch'!!!!" - echo "*** You have probably merged master into '$branch' by mistake" - echo "***" - exit 1 + THIS_SCRIPT=`git rev-parse --git-path hooks/pre-push` + if git show master:scripts/pre-push | diff -q $THIS_SCRIPT - > /dev/null 2>&1 + then + echo "$0 says:" + echo "***" + echo "*** INVALID MERGE: Commit $MASTER_ONLY should not be reachable from '$branch'!!!!" + echo "*** You have probably merged master into '$branch' by mistake" + echo "***" + exit 1 + else + echo "$0 says:" + echo "***" + echo "*** The script '$THIS_SCRIPT' of this OTP repo needs updating." + echo "*** Do it by executing the following command:" + echo "***" + echo "*** git show master:scripts/pre-push > $THIS_SCRIPT" + echo "***" + echo "*** And then retry the push." + echo "***" + exit 1 + fi fi if [ ${remote_ref#refs/heads/maint-} != $remote_ref ] && git merge-base --is-ancestor refs/remotes/$remote/maint $local_sha then |