ref: c98132e30e01a9638e61bd888c769d30e4e43ad5
parent: 33e9d79b78b32d0cc19693ab3c29ba9941d80f8f
author: Bjørn Erik Pedersen <bjorn.erik.pedersen@gmail.com>
date: Thu Oct 8 15:32:53 EDT 2020
Add merge helper
--- /dev/null
+++ b/merge-release.sh
@@ -1,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}";+
+