diff options
| author | Pierre-Marie Pédrot | 2021-02-02 19:59:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-02-02 19:59:48 +0100 |
| commit | bf1d9fcdb8f42f00c198c266a509de0bcf0293f7 (patch) | |
| tree | f6035fc7d80b0d5e41ade55e239579abb93cff82 /dev | |
| parent | 4ae11ea2bf09fcdf44b1226a45761a2aed34a445 (diff) | |
| parent | 2284e8481e7eb3489ff25b5f5c896c7b95c383ee (diff) | |
Merge PR #13791: Bench: don't uselessly rely on initialized opam
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/bench/gitlab-bench.yml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/dev/bench/gitlab-bench.yml b/dev/bench/gitlab-bench.yml index 25545cf565..69136ee773 100644 --- a/dev/bench/gitlab-bench.yml +++ b/dev/bench/gitlab-bench.yml @@ -4,9 +4,7 @@ bench: when: manual before_script: - printenv -0 | sort -z | tr '\0' '\n' - script: - - . ~/.opam/opam-init/init.sh - - ./dev/bench/gitlab.sh + script: dev/bench/gitlab.sh tags: - timing variables: |