mathlib3
1b13ccdf - chore(scripts/deploy_docs.sh): skip gen_docs if already built (#2263)

Commit

5 years ago

chore(scripts/deploy_docs.sh): skip gen_docs if already built (#2263) * chore(scripts/deploy_docs.sh): skip gen_docs if already built * Update scripts/deploy_docs.sh

References

#2263 - chore(scripts/deploy_docs.sh): skip gen_docs if already built

Author

bryangingechen

Parents

211c5d11

mathlib3 1b13ccdf - chore(scripts/deploy_docs.sh): skip gen_docs if already built (#2263)

mathlib3
1b13ccdf - chore(scripts/deploy_docs.sh): skip gen_docs if already built (#2263)