diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-07-15 15:23:02 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-07-21 15:02:46 +0200 |
| commit | 6ea07bb51a935e8f6292a1c84b55cb7a273a6c70 (patch) | |
| tree | f82c647e536631900f1ff23f629a6149db2c1fe1 /plugins/ssrmatching/ssrmatching.mli | |
| parent | 4d858df22bb30d2efbef39a177c28c15c600c885 (diff) | |
Add [opam update] and online repository to gitlab CI script.
This allows it to find out about new packages / compilers without
having to invalidate cache somehow.
Additionally the latest camlp5 (7.01) is not in the local repository
for some reason.
Diffstat (limited to 'plugins/ssrmatching/ssrmatching.mli')
0 files changed, 0 insertions, 0 deletions