Skip to content
Snippets Groups Projects
Commit 6d0aec5a authored by Janno's avatar Janno
Browse files

Disable make quick in CI

parent 8edcc363
No related branches found
No related tags found
No related merge requests found
Pipeline #
...@@ -21,23 +21,23 @@ iris: ...@@ -21,23 +21,23 @@ iris:
only: only:
- master - master
vio: # vio:
stage: quickbuild # stage: quickbuild
tags: # tags:
- coq # - coq
script: > # script: >
cd coq/ra/; # cd coq/ra/;
coqc -v; # coqc -v;
time make -j8 TIMED=y quick 2>&1 | tee build-log-vio.txt; # time make -j8 TIMED=y quick 2>&1 | tee build-log-vio.txt;
cat build-log-vio.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio.txt # cat build-log-vio.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio.txt
only: # only:
- master # - master
cache: # cache:
paths: # paths:
- coq/ra/*.vio # - coq/ra/*.vio
artifacts: # artifacts:
paths: # paths:
- coq/ra/build-time-vio.txt # - coq/ra/build-time-vio.txt
# vio2vo: # vio2vo:
# stage: quickcheck # stage: quickcheck
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment