diff options
| author | Gaëtan Gilbert | 2021-01-26 14:11:48 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-02-02 15:11:22 +0100 |
| commit | 2284e8481e7eb3489ff25b5f5c896c7b95c383ee (patch) | |
| tree | f6035fc7d80b0d5e41ade55e239579abb93cff82 | |
| parent | 4ae11ea2bf09fcdf44b1226a45761a2aed34a445 (diff) | |
Bench: don't uselessly rely on initialized opam
AFAICT this init.sh call is useless.
| -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: |