diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 6ce0d7edd9f47192d7bdd68e09636b3fd44f4ff9..ba435ebe0cd1321c0dc62865c73d15332f8c162f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -36,3 +36,6 @@ stdpp-coq8.6: - master - ci - timing + artifacts: + paths: + - build-time.txt