.github: Ensure that docs are still published on merges/autopushes to…

… master, even if CI has already been ran
uf-mil · Sep 25, 2024 · 2c5700a · 2c5700a
1 parent e494b1f
commit 2c5700a
Showing 1 changed file with 6 additions and 3 deletions.
diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
@@ -112,9 +112,12 @@ jobs:
   deploy-docs:
     name: Deploy docs from master
     runs-on: self-hosted
-    needs:
-      - super-ci
-    if: github.ref == 'refs/heads/master'
+    needs: super-ci
+    # https://github.com/actions/runner/issues/491#issuecomment-850884422
+    if: |
+      always() &&
+      (needs.super-ci.result == 'skipped' || needs.super-ci.result == 'success') &&
+      github.ref == 'refs/heads/master'
     steps:
       - name: Checkout
         uses: actions/checkout@v4