attempt to fix master CI (#84)
parent
64f627a295
commit
72227e4b11
|
@ -30,16 +30,19 @@ jobs:
|
||||||
cd mathlib4
|
cd mathlib4
|
||||||
lake build
|
lake build
|
||||||
|
|
||||||
- name: generate docs, deploy if on master
|
- name: generate docs (PRs only)
|
||||||
|
if: github.event_name == 'pull_request'
|
||||||
run: |
|
run: |
|
||||||
if [ "$github_repo" = "leanprover/doc-gen4" ] && [ "$github_ref" = "refs/heads/main" ]; then
|
|
||||||
deploy="true"
|
|
||||||
DOC_GEN_REF="main"
|
|
||||||
else
|
|
||||||
deploy="false"
|
|
||||||
fi
|
|
||||||
cd ../
|
cd ../
|
||||||
./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "$deploy" "LeanInk"
|
./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "false" "LeanInk"
|
||||||
|
env:
|
||||||
|
DOC_GEN_REF: ${{ github.event.pull_request.head.sha }}
|
||||||
|
|
||||||
|
- name: generate and deploy docs (master only)
|
||||||
|
if: github.event_name == 'push' && github.repository == 'leanprover/doc-gen4'
|
||||||
|
run: |
|
||||||
|
cd ../
|
||||||
|
./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "true" "LeanInk"
|
||||||
env:
|
env:
|
||||||
MATHLIB4_DOCS_KEY: ${{ secrets.MATHLIB4_DOCS_KEY }}
|
MATHLIB4_DOCS_KEY: ${{ secrets.MATHLIB4_DOCS_KEY }}
|
||||||
DOC_GEN_REF: ${{ github.event.pull_request.head.sha }}
|
DOC_GEN_REF: "main"
|
||||||
|
|
Loading…
Reference in New Issue