Add merge helper

This commit is contained in:
Bjørn Erik Pedersen 2020-10-08 19:32:53 +02:00
parent 33e9d79b78
commit c98132e30e
No known key found for this signature in database
GPG Key ID: 330E6E2BD4859D8F
1 changed files with 23 additions and 0 deletions

23
merge-release.sh Executable file
View File

@ -0,0 +1,23 @@
#!/usr/bin/env bash
if (( $# < 1 ));
then
echo "USAGE: ./merge-release.sh 0.76.0"
exit 1
fi
die() { echo "$*" 1>&2 ; exit 1; }
v=$1
git merge "release-${v}" || die;
git push || die;
git checkout stable || die;
git reset --hard "v${v}" || die;
git push -f || die;
git checkout master || die;
git subtree push --prefix=docs/ docs-local "tempv${v}";