From 0760d619677750c48aa7e1d85dc259f36c5964c8 Mon Sep 17 00:00:00 2001 From: grunweg Date: Wed, 18 Dec 2024 14:40:38 +0100 Subject: [PATCH] chore: also copy 1000.yaml Pre-requisite for leanprover-community.github.io#/558. --- .github/workflows/docs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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: |