diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 61f334ab22b923811cac3f56eea7a0e6c8067a63..1bafef34be82937b64e8d2be289d80b2907d30ff 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -39,21 +39,21 @@ vio: paths: - coq/ra/build-time-vio.txt -vio2vo: - stage: quickcheck - tags: - - coq - script: > - cd coq/ra/; - coqc -v; - time make -j8 TIMED=y vio2vo J=8 2>&1 | tee build-log-vio2vo.txt; - cat build-log-vio2vo.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio2vo.txt - only: - - master - allow_failure: true - artifacts: - paths: - - coq/ra/build-time-vio2vo.txt +# vio2vo: +# stage: quickcheck +# tags: +# - coq +# script: > +# cd coq/ra/; +# coqc -v; +# time make -j8 TIMED=y vio2vo J=8 2>&1 | tee build-log-vio2vo.txt; +# cat build-log-vio2vo.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio2vo.txt +# only: +# - master +# allow_failure: true +# artifacts: +# paths: +# - coq/ra/build-time-vio2vo.txt full: stage: fullbuild