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

Merged

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

mergify merged 2 commits into master from skip_gen_docs

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

f46dbb0a

bryangingechen commented on 2020-03-28

Update scripts/deploy_docs.sh

0a63a7f5

kim-em approved these changes on 2020-03-28

kim-em added ready-to-merge

mergify merged 1b13ccdf into master 5 years ago

bryangingechen deleted the skip_gen_docs branch 5 years ago

Reviewers

kim-em

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone