add --push flag to mike deploy

cioos-siooc · Aug 15, 2023 · fe5f58a · fe5f58a
1 parent 6a8af6b
commit fe5f58a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/.github/workflows/deploy-docs.yaml b/.github/workflows/deploy-docs.yaml
@@ -32,8 +32,8 @@ jobs:
           git config --global user.email "${GITHUB_ACTOR}@users.noreply.github.com"
       - run: |
           if [[ "${{github.ref_name}}" == "main" ]]; then
-              mike deploy main 
+              mike deploy main --push
           else
-              mike deploy dev
+              mike deploy dev --push
           fi
           mike set-default dev