fix : CI
parent
b18f4e52ed
commit
07332cad93
|
@ -21,10 +21,6 @@ jobs:
|
|||
~/.elan/bin/lean --version
|
||||
echo "$HOME/.elan/bin" >> $GITHUB_PATH
|
||||
|
||||
- name: compile doc-gen4
|
||||
run: |
|
||||
lake build
|
||||
|
||||
- name: Checkout and compile mathlib4
|
||||
run: |
|
||||
cd ../
|
||||
|
@ -32,7 +28,7 @@ jobs:
|
|||
cd mathlib4
|
||||
lake build
|
||||
|
||||
- name: generate and deploy docs
|
||||
- name: generate docs, deploy if on master
|
||||
run: |
|
||||
if [ "$github_repo" = "leanprover/doc-gen4" ] && [ "$github_ref" = "refs/heads/main" ]; then
|
||||
deploy="true"
|
||||
|
|
|
@ -23,7 +23,8 @@ fi
|
|||
|
||||
# generate the docs
|
||||
cd $1
|
||||
lake -Kenv=dev build Mathlib:docs --verbose
|
||||
sed -i "s/git \"https:\/\/github.com\/leanprover\/doc-gen4\" @ \"main\"/\"..\" \/ \"$2\" with NameMap.empty/" lakefile.lean
|
||||
lake -Kdoc=on build Mathlib:docs --verbose
|
||||
|
||||
if [ "$3" = "true" ]; then
|
||||
cd ..
|
||||
|
|
Loading…
Reference in New Issue