diff options
| -rw-r--r-- | .gitlab-ci.yml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8880ec1d21..f439b0c34f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -212,7 +212,10 @@ before_script: dependencies: - not-a-real-job script: - - cd _install_ci + # exit 0: workaround for https://gitlab.com/gitlab-org/gitlab/issues/202505 + # the validate:quick job is sometimes started before build:quick, without artifacts + # we ignore these spurious errors so if the job fails it's a real error + - cd _install_ci || exit 0 - 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 |