diff options
| author | Emilio Jesus Gallego Arias | 2019-02-04 19:41:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-04 19:41:45 +0100 |
| commit | f177aa562ee76c1607350306363aaf844e48d07e (patch) | |
| tree | a3bce46ce35757aed1a56e4c9e3b818bbba78a0a /dev/tools | |
| parent | c70412ec8b0bb34b7a5607c07d34607a147d834c (diff) | |
| parent | 5cf7224c1cd7507eabe415951faad687e0a8f119 (diff) | |
Merge PR #9468: Remove AppVeyor: superseded by Azure.
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
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 |