tweak push.sh release script

mpenkov · mpenkov · commit 83a67af45a3a · 2021-09-11T23:07:28.000+09:00
diff --git a/release/push.sh b/release/push.sh
@@ -3,5 +3,9 @@
 #
 # Run this after you've verified the results of merge.sh.
 #
+set -euxo pipefail
+release=$RELEASE
+
 git push --tags upstream master
 git push upstream develop
+git push upstream release-"$release"

Original file line number	Diff line number	Diff line change
`@@ -3,5 +3,9 @@`
`3`	`3`	`#`
`4`	`4`	`# Run this after you've verified the results of merge.sh.`
`5`	`5`	`#`
	`6`	`+set -euxo pipefail`
	`7`	`+release=$RELEASE`
	`8`	`+`
`6`	`9`	`git push --tags upstream master`
`7`	`10`	`git push upstream develop`
	`11`	`+git push upstream release-"$release"`