aboutsummaryrefslogtreecommitdiff
path: root/.travis.yml
diff options
context:
space:
mode:
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml4
1 files changed, 2 insertions, 2 deletions
diff --git a/.travis.yml b/.travis.yml
index de21f52bb..58c9f29fb 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -124,10 +124,10 @@ jobs:
- stage: standalone-ocaml
env: COQ_VERSION="8.8.0" COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"
- script: PREV=4 CUR=5 ./etc/ci/travis.sh standalone-ocaml c-files
+ script: PREV=4 CUR=5 ./etc/ci/travis.sh standalone-ocaml c-files test-c-files CC=gcc
- stage: standalone-ocaml
env: COQ_VERSION="8.7.2" COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
- script: PREV=4 CUR=5 ./etc/ci/travis.sh standalone-ocaml c-files
+ script: PREV=4 CUR=5 ./etc/ci/travis.sh standalone-ocaml c-files test-c-files CC=gcc
# - stage: selected-test selected-bench
# env: COQ_VERSION="8.8.0" COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"