diff options
| author | Maxime Dénès | 2017-10-06 12:33:05 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-06 12:33:05 +0200 |
| commit | 6bfa989253a3ec5563b07c5b14661d6b8dfebd6b (patch) | |
| tree | 47932248c439d3c84674250f78d76405d7fc89e3 | |
| parent | 084ef10a464a578f5378a7c184348e68a2efdb43 (diff) | |
| parent | 2b33af7d4572122f585c8826e60fbe51db602551 (diff) | |
Merge PR #1128: GitLab CI: make all_stdlib.v in build job
| -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 ae55302d11..d2e335d45a 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' |