diff options
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c3627862e3..f8b0f94716 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -170,7 +170,7 @@ after_script: - cd _install_ci - find lib/coq/ -name '*.vo' -print0 > vofiles - for regexp in 's/.vo//' 's:lib/coq/plugins:Coq:' 's:lib/coq/theories:Coq:' 's:/:.:g'; do sed -z -i "$regexp" vofiles; done - - xargs -0 --arg-file=vofiles bin/coqchk -boot -silent -o -m -coqlib lib/coq/ + - xargs -0 --arg-file=vofiles bin/coqchk -silent -o -m -coqlib lib/coq/ .ci-template: &ci-template stage: test |