mathlib3
feat(ci): avoid push to Azure if branch has been updated
#2048

Merged

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

mergify merged 9 commits into master from avoid-azure-push

avoid push to Azure if branch has been updated

3499e70e

robertylewis changed the title ~~avoid push to Azure if branch has been updated~~ feat(ci): avoid push to Azure if branch has been updated 6 years ago

changes to git config in deploy_nightly.sh break git fetch

41cb3e52

I don't understand why this is different than on my own repo

209cf01d

artifact upload breaks fetch, I guess?

6b6fd2b0

factor out git config

6a0a15e4

fix env variable

03ada34e

gebner commented on 2020-02-25

adjustments

32b94ee6

removed repo check

bd4e3697

robertylewis added awaiting-review

kim-em commented on 2020-02-26

kim-em removed awaiting-review

kim-em added ready-to-merge

kim-em approved these changes on 2020-02-27

Merge branch 'master' into avoid-azure-push

7213bce7

mergify merged 0e4eb09d into master 6 years ago

mergify deleted the avoid-azure-push branch 6 years ago

Reviewers

kim-em

gebner

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(ci): avoid push to Azure if branch has been updated #2048 Merged

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

mathlib3
feat(ci): avoid push to Azure if branch has been updated
#2048

Merged