diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index 818bf1ff4b8..9e647ee21d6 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -96,7 +96,7 @@ jobs: - name: copy extra files run: | - cp mathlib4/docs/{100.yaml,overview.yaml,undergrad.yaml} workaround/.lake/build/doc + cp mathlib4/docs/{100.yaml,1000.yaml,overview.yaml,undergrad.yaml} workaround/.lake/build/doc - name: copy import graph run: |