diff options
| author | Maxime Dénès | 2017-11-24 12:46:57 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-24 12:46:57 +0100 |
| commit | 31794a1828a15acb95c235fd3166c511635add41 (patch) | |
| tree | fb09a6b201001ababc3030dc80fa9d729526c0a7 /dev/ci | |
| parent | 92c15a9b660b874ce3fa125b1f9bdf2e85c40f47 (diff) | |
| parent | 57f62f06419972ba799e451d2f56552dc1b2fb63 (diff) | |
Merge PR #6197: [plugin] Remove LocalityFixme über hack.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh new file mode 100644 index 0000000000..c9f1272bed --- /dev/null +++ b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6197" ] || [ "$TRAVIS_BRANCH" = "plugins+remove_locality_hack" ]; then + ltac2_CI_BRANCH=localityfixyou + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2.git +fi |