From 07332cad933b907f00604bd7d224ea1954c85f73 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 18 Aug 2022 21:28:55 +0200
Subject: [PATCH] fix : CI

---
 .github/workflows/build.yml | 6 +-----
 deploy_docs.sh              | 3 ++-
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 8f961d9..4387a4f 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -21,10 +21,6 @@ jobs:
           ~/.elan/bin/lean --version
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      - name: compile doc-gen4
-        run: |
-          lake build
-
       - name: Checkout and compile mathlib4
         run: |
           cd ../
@@ -32,7 +28,7 @@ jobs:
           cd mathlib4
           lake build
 
-      - name: generate and deploy docs
+      - name: generate docs, deploy if on master
         run: |
           if [ "$github_repo" = "leanprover/doc-gen4" ] && [ "$github_ref" = "refs/heads/main" ]; then
             deploy="true"
diff --git a/deploy_docs.sh b/deploy_docs.sh
index 6042795..bfed993 100755
--- a/deploy_docs.sh
+++ b/deploy_docs.sh
@@ -23,7 +23,8 @@ fi
 
 # generate the docs
 cd $1
-lake -Kenv=dev build Mathlib:docs --verbose
+sed -i "s/git \"https:\/\/github.com\/leanprover\/doc-gen4\" @ \"main\"/\"..\" \/ \"$2\" with NameMap.empty/" lakefile.lean
+lake -Kdoc=on build Mathlib:docs --verbose
 
 if [ "$3" = "true" ]; then
   cd ..