diff options
| author | Théo Zimmermann | 2020-04-17 14:32:02 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-17 14:32:02 +0200 |
| commit | f3af9a4c6e6813f32dfe632209e145ffbf5fed98 (patch) | |
| tree | 44632df517b713a6bd487445e433dab9b9d98e16 | |
| parent | 87f8c9fce73ebf8bc0b6cb53536bdb3861f09e41 (diff) | |
| parent | 633b462dc0c0211d353faebc6acbe6393c1566b6 (diff) | |
Merge PR #12111: CI: Ignore spurious errors in validate jobs
Reviewed-by: Zimmi48
| -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 |