Skip to content

Commit

Permalink
Remove workaround for validate:vio early start
Browse files Browse the repository at this point in the history
Let's see if this still happens
  • Loading branch information
SkySkimmer committed Dec 7, 2023
1 parent 411b0e8 commit 36f2b65
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions .gitlab-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -165,10 +165,10 @@ before_script:
needs:
- not-a-real-job
script:
# exit 0: workaround for https://gitlab.com/gitlab-org/gitlab/issues/202505
# put || exit 0 as a workaround if https://gitlab.com/gitlab-org/gitlab/issues/202505 reoccurs
# the validate:vio job is sometimes started before build:vio, without artifacts
# we ignore these spurious errors so if the job fails it's a real error
- cd _install_ci || exit 0
- cd _install_ci
- 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
Expand Down

0 comments on commit 36f2b65

Please sign in to comment.