diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-07 13:22:59 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-07 13:22:59 +0200 |
| commit | adfc3cebf405f599292c7c8f131620837f0af93f (patch) | |
| tree | 06a97672fa4e623a23d7abe9556ffbe17fc8536d /.travis.yml | |
| parent | f2b28f819c16ad773ab5a2e426e3c0a478cbfdef (diff) | |
Remove cross-crypto from Travis. It is still tested in GitLab CI.
This fixes #7734.
Diffstat (limited to '.travis.yml')
| -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="" |