From c98132e30e01a9638e61bd888c769d30e4e43ad5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B8rn=20Erik=20Pedersen?=
 <bjorn.erik.pedersen@gmail.com>
Date: Thu, 8 Oct 2020 19:32:53 +0200
Subject: [PATCH] Add merge helper

---
 merge-release.sh | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100755 merge-release.sh

diff --git a/merge-release.sh b/merge-release.sh
new file mode 100755
index 000000000..a87f9f4a1
--- /dev/null
+++ b/merge-release.sh
@@ -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}";
+
+