chore: fix docbuild setup

fpvandoorn · Jan 6, 2025 · 558aff7 · 558aff7
1 parent 88d85ba
commit 558aff7
Show file tree

Hide file tree

Showing 4 changed files with 2 additions and 156 deletions.
diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
@@ -76,7 +76,7 @@ jobs:
       - name: Build project documentation
         working-directory: docbuild
         run: |
-          ~/.elan/bin/lake update carleson || true
+          MATHLIB_NO_CACHE_ON_UPDATE=1 ~/.elan/bin/lake update carleson || true
           ~/.elan/bin/lake build Carleson:docs
 
       - name: Build blueprint and copy to `docs/blueprint`

diff --git a/.github/workflows/push_pr.yml b/.github/workflows/push_pr.yml
@@ -41,8 +41,7 @@ jobs:
       - name: Test carleson update in docbuild
         working-directory: docbuild
         run: |
-          ~/.elan/bin/lake update carleson || true
-          #~/.elan/bin/lake build Carleson:docs
+          MATHLIB_NO_CACHE_ON_UPDATE=1 ~/.elan/bin/lake update carleson || true
 
       - name: Build blueprint and copy to `docs/blueprint`
         uses: xu-cheng/texlive-action@v2

diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json
diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain