.github: move pushing to dist script

.github/workflows/dist-docs.yml

@@ -92,8 +92,7 @@ jobs:
           git config user.name "github-actions[bot]"
           git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
           if [ "$IS_TAG" = "true" ]; then
-            ./scripts/dist/docs.sh --noconfirm
+            ./scripts/dist/docs.sh --noconfirm --push
           else
-            ./scripts/dist/docs.sh --noconfirm master
+            ./scripts/dist/docs.sh --noconfirm --push master
           fi
-          git push origin gh-pages

scripts/dist/docs.sh

@@ -7,6 +7,7 @@ set -eu
 . scripts/dist/version.sh
 
 NOCONFIRM=0
+PUSH=0
 ARGS=()
 
 while [ $# -gt 0 ]; do
@@ -16,6 +17,7 @@ while [ $# -gt 0 ]; do
 		echo ""
 		echo "Options:"
 		echo "  --noconfirm  Skip any user confirmations."
+		echo "  --push       Push changes to remote."
 		echo ""
 		exit 0
 		;;
@@ -23,6 +25,10 @@ while [ $# -gt 0 ]; do
 		NOCONFIRM=1
 		shift
 		;;
+	--push)
+		PUSH=1
+		shift
+		;;
 	-*)
 		echo "Unknown option $1"
 		exit 1
@@ -81,3 +87,7 @@ fi
 
 # Commit changes.
 git commit -m "Docs ${VERSION}" || exit 0
+
+if [ "${PUSH}" -eq 1 ]; then
+	git push origin gh-pages
+fi