~stepbrobd/coq: Bench: do not save profiles from OLD as artifacts

7e8b7626c955e35358c6b1615f287e5b336e389c — Gaëtan Gilbert a month ago cb7bd30

Bench: do not save profiles from OLD as artifacts

We are getting close to the 500MB compressed limit for artifacts, this
should help.

patch browse .tar.gz

1 files changed, 0 insertions(+), 1 deletions(-)

M dev/bench/gitlab-bench.yml

M dev/bench/gitlab-bench.yml => dev/bench/gitlab-bench.yml +0 -1

@@ 22,7 22,6 @@ bench:
       - _bench/opam.NEW/**/*.prof.json.gz
       - _bench/opam.OLD/**/*.log
       - _bench/opam.OLD/**/*.timing
-      - _bench/opam.OLD/**/*.prof.json.gz
     when: always
     expire_in: 1 year
   environment: bench