Adjust documentation push for master -> main

chad-iris · chad-iris · commit 1c83bbe2ae1e · 2022-12-04T14:18:40.000-08:00
diff --git a/doc/build-push-docs.sh b/doc/build-push-docs.sh
@@ -97,4 +97,4 @@ git commit -m 'committing documentation'
 git remote add origin $GITREMOTE
 
 echo "Pushing contents of $BASEDIR/$DOCDIR to $GITREMOTE branch gh-pages"
-git push --quiet --force origin master:gh-pages
+git push --quiet --force origin main:gh-pages
