diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b9c42e0b3fad80cd18f25246dd1733fafbc775ce..de940fb80884ee9c469acb12bd8b4ccf9563cf3e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -12,9 +12,9 @@ vio: script: | cd coq/ra/ coqc -v - 'time make -j8 TIMED=y quick 2>&1 | tee build-log-vio.txt' - 'fgrep Axiom build-log.txt && exit 1' - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-quick.txt' + time make -j8 TIMED=y quick 2>&1 | tee build-log-vio.txt + fgrep Axiom build-log.txt && exit 1 + cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-quick.txt only: - master artifacts: @@ -26,11 +26,11 @@ vio2vo: tags: - coq script: | - 'cd coq/ra/' + cd coq/ra/ coqc -v - 'time make -j8 TIMED=y vio2vo J=8 2>&1 | tee build-log-vio2vo.txt' - 'fgrep Axiom build-log.txt && exit 1' - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-quick.txt' + time make -j8 TIMED=y vio2vo J=8 2>&1 | tee build-log-vio2vo.txt + fgrep Axiom build-log.txt && exit 1 + cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-quick.txt only: - master artifacts: @@ -42,12 +42,12 @@ full: tags: - coq script: | - 'cd coq/ra/' + cd coq/ra/ coqc -v - 'make clean' - 'time make -j8 TIMED=y 2>&1 | tee build-log-full.txt' - 'fgrep Axiom build-log.txt && exit 1' - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-quick.txt' + make clean' + time make -j8 TIMED=y 2>&1 | tee build-log-full.txt + fgrep Axiom build-log.txt && exit 1 + cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-quick.txt only: - master artifacts: