fix: attempt to fix CI again

main
Henrik Böving 2023-01-01 20:37:05 +01:00
parent a18b27f4c1
commit dd5aae412d
1 changed files with 1 additions and 1 deletions

View File

@ -45,4 +45,4 @@ jobs:
./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "true" "LeanInk" ./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: "main" DOC_GEN_REF: ${{ github.sha }}