fix: new lake directories

leanprover-community · Nov 18, 2023 · cd14aeb · cd14aeb
1 parent 1f4ea76
commit cd14aeb
Showing 1 changed file with 4 additions and 4 deletions.
diff --git 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