diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-05 18:43:08 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-05 18:44:08 +0200 |
| commit | 2b33af7d4572122f585c8826e60fbe51db602551 (patch) | |
| tree | 611f6f7054442439a3d1c6006f59dda534d42401 /.gitlab-ci.yml | |
| parent | 85b1deda0348f1fd32f7019fb1e7bfabd297a751 (diff) | |
GitLab CI: make all_stdlib.v in build job
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' |