Commit 51f6f15d710c39c6844ceef58efea6db93c46d61

Edward Thomson 2021-11-09T09:03:06

ci: only update docs on push Only update the documentation on a `push`. We were previously updating the documentation only when not in a `pull_request`, which meant that we would push documentation updates in manual build triggers.

1
2
3
4
5
6
7
8
9
10
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 572f025..e805b1b 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -300,4 +300,4 @@ jobs:
     - name: Push documentation branch
       working-directory: source
       run: git push origin gh-pages
-      if: github.event_name != 'pull_request' && github.repository == 'libgit2/libgit2'
+      if: github.event_name == 'push' && github.repository == 'libgit2/libgit2'