diff options
| author | Emilio Jesus Gallego Arias | 2019-05-10 13:31:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-10 13:31:41 +0200 |
| commit | c659b96eaa7bb5e401786546bb293a31e5f3c3d4 (patch) | |
| tree | d8f7f85a9ea2013453cd2b800d86fb28727aa331 | |
| parent | f913913a6a1b1e01d154d0c9af3b3807459b0b9f (diff) | |
| parent | c12c4a01e46aacb97ea3d34047a10d17630baba4 (diff) | |
Merge PR #10065: CI: run coqchk without -silent
| -rw-r--r-- | .gitlab-ci.yml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e4815920ce..9e96d3602b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -169,7 +169,15 @@ before_script: - not-a-real-job script: - cd _install_ci - - find lib/coq/ -name '*.vo' -print0 | xargs -0 bin/coqchk -silent -o -m -coqlib lib/coq/ + - find lib/coq/ -name '*.vo' -fprint0 vofiles + - xargs -0 --arg-file=vofiles bin/coqchk -o -m -coqlib lib/coq/ > ../coqchk.log 2>&1 || touch coqchk.failed + - tail -n 1000 ../coqchk.log # the log is too big for gitlab so pipe to a file and display the tail + - "[ ! -f coqchk.failed ]" # needs quoting for yml syntax reasons + artifacts: + name: "$CI_JOB_NAME.logs" + paths: + - coqchk.log + expire_in: 1 month .ci-template: stage: test |