diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-04 23:55:24 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-07 10:27:17 +0100 |
| commit | 138a4da7f0133d7b4ea06cfbc938d23ddb88c97d (patch) | |
| tree | 8f54418ccec857d9d5dea108ccaed0cf8de221de /.travis.yml | |
| parent | 3a66f149a34613ef0ed04046fed3947e8e720cd6 (diff) | |
[travis] [External CI] Script renaming.
Diffstat (limited to '.travis.yml')
| -rw-r--r-- | .travis.yml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/.travis.yml b/.travis.yml index 14573e295..c85122ac9 100644 --- a/.travis.yml +++ b/.travis.yml @@ -21,9 +21,9 @@ env: # Main test suites matrix: - TEST_TARGET="validate" TW="travis_wait" - - TEST_TARGET="contrib-hott" - - TEST_TARGET="contrib-math-comp" - - TEST_TARGET="contrib-compcert" + - TEST_TARGET="ci-hott" + - TEST_TARGET="ci-math-comp" + - TEST_TARGET="ci-compcert" matrix: |