fix: make lake preserve toolchain for docs (#1086)

leanprover-community · Jan 5, 2025 · 03f408f · 03f408f
1 parent 101795c
commit 03f408f
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/.github/workflows/docs-deploy.yml b/.github/workflows/docs-deploy.yml
@@ -26,7 +26,7 @@ jobs:
 
       - name: Build Docs
         working-directory: docs
-        run: lake build -q Batteries:docs
+        run: lake build --keep-toolchain -q Batteries:docs
 
       - name: Deploy Docs
         run: |

diff --git a/.github/workflows/docs-release.yml b/.github/workflows/docs-release.yml
@@ -27,7 +27,7 @@ jobs:
 
       - name: Build Docs
         working-directory: docs
-        run: lake build -q Batteries:docs
+        run: lake build --keep-toolchain -q Batteries:docs
 
       - name: Compress Docs
         working-directory: docs