From 72227e4b11647896648a8e2bfb5119357b1f5ae0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 5 Oct 2022 13:00:43 +0200
Subject: [PATCH] attempt to fix master CI (#84)

---
 .github/workflows/build.yml | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 67cde95..3fe55fd 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -30,16 +30,19 @@ jobs:
           cd mathlib4
           lake build
 
-      - name: generate docs, deploy if on master
+      - name: generate docs (PRs only)
+        if: github.event_name == 'pull_request'
         run: |
-          if [ "$github_repo" = "leanprover/doc-gen4" ] && [ "$github_ref" = "refs/heads/main" ]; then
-            deploy="true"
-            DOC_GEN_REF="main"
-          else
-            deploy="false"
-          fi
           cd ../
-          ./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "$deploy" "LeanInk"
+          ./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "false" "LeanInk"
+        env:
+          DOC_GEN_REF: ${{ github.event.pull_request.head.sha }}
+
+      - name: generate and deploy docs (master only)
+        if: github.event_name == 'push' && github.repository == 'leanprover/doc-gen4'
+        run: |
+          cd ../
+          ./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "true" "LeanInk"
         env:
           MATHLIB4_DOCS_KEY: ${{ secrets.MATHLIB4_DOCS_KEY }}
-          DOC_GEN_REF: ${{ github.event.pull_request.head.sha }}
+          DOC_GEN_REF: "main"