mathlib3
edd02097 - ci(deploy_docs.sh): generalize for use in doc-gen CI (#2978)

Commit
5 years ago
ci(deploy_docs.sh): generalize for use in doc-gen CI (#2978) This moves some installation steps out of `deploy_docs.sh` script and makes it accept several path arguments so that it can be re-used in the CI for `doc-gen`. The associated `doc-gen` PR: https://github.com/leanprover-community/doc-gen/pull/27 will be updated after this is merged.
Parents
Loading