push deployed doc as well..

soot-oss · Nov 2, 2023 · d6279ab · d6279ab
1 parent 7296b9a
commit d6279ab
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml
@@ -3,6 +3,7 @@
 # mike set-default latest --push
 
 name: Documentation
+
 on:
   push:
     branches:
@@ -70,7 +71,7 @@ jobs:
       # on PR events..
       - name: deploy doc in subdirectory
         if: github.event_name == 'pull_request'
-        run: mike deploy ${{ github.head_ref }}_preview
+        run: mike deploy ${{ github.head_ref }}_preview --push
         # TODO: set to true when the release is capable of the documentation ;)  && mike props ${{ github.head_ref }}_preview --set-string hidden=true --push
 
       - name: comment link to preview

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -1,11 +1,11 @@
+name: Create Release Draft
+
 on:
   push:
     tags:
       # Push events to matching
       - ^v(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)$
 
-name: Create Release Draft
-
 jobs:
   build:
     name: Create Release Draft