feat: Add todo list to docs
This commit is contained in:
parent
678a35899d
commit
594020f0e8
2 changed files with 11 additions and 4 deletions
11
.github/workflows/docs.yml
vendored
11
.github/workflows/docs.yml
vendored
|
@ -30,14 +30,14 @@ jobs:
|
|||
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
|
||||
~/.elan/bin/lean --version
|
||||
echo "$HOME/.elan/bin" >> $GITHUB_PATH
|
||||
|
||||
- name: Get cache
|
||||
|
||||
- name: Get Mathlib cache
|
||||
run: lake -Kenv=dev exe cache get || true
|
||||
|
||||
- name: Build project
|
||||
run: lake -Kenv=dev build HepLean
|
||||
|
||||
- name: Cache mathlib docs
|
||||
- name: Get doc cache
|
||||
uses: actions/cache@v3
|
||||
with:
|
||||
path: |
|
||||
|
@ -57,7 +57,10 @@ jobs:
|
|||
|
||||
- name: Build documentation
|
||||
run: lake -Kenv=dev build HepLean:docs
|
||||
|
||||
|
||||
- name: make TODO list
|
||||
run : lake exe find_TODOs mkFile
|
||||
|
||||
- name: Copy documentation to `docs/docs`
|
||||
run: |
|
||||
mv .lake/build/doc docs/docs
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue