mathlib
0e4eb09d - feat(ci): avoid push to Azure if branch has been updated (#2048)

Commit
5 years ago
feat(ci): avoid push to Azure if branch has been updated (#2048) * avoid push to Azure if branch has been updated * changes to git config in deploy_nightly.sh break git fetch * I don't understand why this is different than on my own repo * artifact upload breaks fetch, I guess? * factor out git config * fix env variable * adjustments * removed repo check Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading