diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-07 13:27:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-07 13:27:57 +0200 |
| commit | 54abefa048519c160c61f0f1c217d658ad0d3aaa (patch) | |
| tree | eb13dcdf8c9b0fae233c8865bf0546664b534d81 | |
| parent | 28ca5295339afecfc4ecb70214f6f575c11e34a1 (diff) | |
| parent | adfc3cebf405f599292c7c8f131620837f0af93f (diff) | |
Merge PR #7735: Remove cross-crypto from Travis. It is still tested in GitLab CI.
| -rw-r--r-- | .travis.yml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/.travis.yml b/.travis.yml index 5c7fc5a33..86a2aea66 100644 --- a/.travis.yml +++ b/.travis.yml @@ -82,9 +82,6 @@ matrix: - TEST_TARGET="ci-coquelicot" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-cross-crypto" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-elpi" EXTRA_OPAM="elpi" # ppx_tools_versioned requires a specific version findlib - FINDLIB_VER="" |