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 /dev/ci/ci-basic-overlay.sh | |
| parent | 4ae11ea2bf09fcdf44b1226a45761a2aed34a445 (diff) | |
Bench: don't uselessly rely on initialized opam
AFAICT this init.sh call is useless.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions