diff options
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ae55302d1..d2e335d45 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -60,6 +60,7 @@ before_script: paths: - _install_ci - config/Makefile + - test-suite/misc/universes/all_stdlib.v expire_in: 1 week script: - set -e @@ -70,6 +71,7 @@ before_script: - echo 'start:coq.build' - make -j ${NJOBS} + - make test-suite/misc/universes/all_stdlib.v - echo 'end:coq:build' - echo 'start:coq.install' |