diff options
| author | Théo Zimmermann | 2019-02-04 18:00:42 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-04 18:00:42 +0100 |
| commit | 5cf7224c1cd7507eabe415951faad687e0a8f119 (patch) | |
| tree | a3bce46ce35757aed1a56e4c9e3b818bbba78a0a /dev/tools | |
| parent | c70412ec8b0bb34b7a5607c07d34607a147d834c (diff) | |
Remove AppVeyor: superseded by Azure.
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/merge-pr.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 72e2930386..813ad71be9 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -143,7 +143,7 @@ fi # Sanity check: PR has an outdated version of CI BASE_COMMIT=$(echo "$PRDATA" | jq -r '.base.sha') -CI_FILES=(".gitlab-ci.yml" "appveyor.yml") +CI_FILES=(".gitlab-ci.yml" "azure-pipelines.yml") if ! git diff --quiet "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}" then |