From cfe90dbed5053c3c011735853d05af50d2e6118c Mon Sep 17 00:00:00 2001
From: Michael Telatynski <7t3chguy@gmail.com>
Date: Thu, 24 Sep 2020 12:47:23 +0100
Subject: [PATCH] Always push docs if they are generated

---
 release.sh | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/release.sh b/release.sh
index e8f7f06c3..a2f59f5fe 100755
--- a/release.sh
+++ b/release.sh
@@ -327,6 +327,7 @@ if [ -z "$skip_jsdoc" ]; then
         $release index.html
     git add "$release"
     git commit --no-verify -m "Add jsdoc for $release" index.html "$release"
+    git push origin gh-pages
 fi
 
 # if it is a pre-release, leave it on the release branch for now.
@@ -341,11 +342,8 @@ git checkout master
 git pull
 git merge "$rel_branch"
 
-# push master and docs (if generated) to github
+# push master to github
 git push origin master
-if [ -z "$skip_jsdoc" ]; then
-    git push origin gh-pages
-fi
 
 # finally, merge master back onto develop (if it exists)
 if [ $(git branch -lr | grep origin/develop -c) -ge 1 ]; then