diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d5a16486709a946d6992b093591d1182120ed196..c5ae0e254eba36360f942965701fcd1fe65e1907 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -13,7 +13,7 @@ variables: - fp-timing script: # prepare - - . build/opam-ci.sh coq $OPAM_PINS + - . build/opam-ci.sh $OPAM_PINS - env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt # build - 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'