From cd14aebb4477e0f5876a1f612c648f401aa00678 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 18 Nov 2023 23:13:06 +0100 Subject: [PATCH] fix: new lake directories --- .github/workflows/docs.yaml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index 2f6ccbc37a1..990901f1db1 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -58,8 +58,8 @@ jobs: git commit -m "workaround" git remote add origin "https://github.com/leanprover/workaround" - mkdir lake-packages - cp -r ../mathlib4/lake-packages/* lake-packages/ + mkdir -p .lake/packages + cp -r ../mathlib4/.lake/packages/* .lake/packages lake update - name: build doc-gen4 @@ -74,12 +74,12 @@ jobs: - name: copy extra files run: | - cp mathlib4/docs/{100.yaml,overview.yaml,undergrad.yaml} workaround/build/doc + cp mathlib4/docs/{100.yaml,overview.yaml,undergrad.yaml} workaround/.lake/build/doc - name: Upload artifact uses: actions/upload-pages-artifact@v1 with: - path: 'workaround/build/doc' + path: 'workaround/.lake/build/doc' - name: Deploy to GitHub Pages id: deployment