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 /lib | |
| parent | 4ae11ea2bf09fcdf44b1226a45761a2aed34a445 (diff) | |
| parent | 2284e8481e7eb3489ff25b5f5c896c7b95c383ee (diff) | |
Merge PR #13791: Bench: don't uselessly rely on initialized opam
Reviewed-by: ppedrot
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions