diff options
| author | Gaëtan Gilbert | 2019-01-22 23:29:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-22 23:32:46 +0100 |
| commit | 95d977bf0b1825b7d822abbdd062cdb8c38051cb (patch) | |
| tree | 930521bfe8d77d5fc11e42d562ea6607cdfe81ec /dev/tools | |
| parent | 03c17218eeacb098ff57ecee1d98f46b7c8fa185 (diff) | |
Remove travis
The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
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 a27dacc5a7..72e2930386 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=(".travis.yml" ".gitlab-ci.yml" "appveyor.yml") +CI_FILES=(".gitlab-ci.yml" "appveyor.yml") if ! git diff --quiet "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}" then |