diff options
| author | Emilio Jesus Gallego Arias | 2019-03-23 17:43:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-23 17:43:35 +0100 |
| commit | ffc088b15b75f0d0577811df48b3511ab9942d1c (patch) | |
| tree | ac85641a010fd7011f49a629df4fcd2b6553828c /dev | |
| parent | 1d68c24736b4cf68ac0c2f70122e3f3d28f0e876 (diff) | |
[ci] [gitlab] Pin ocamlfind to master
https://gitlab.camlcity.org/gerd/lib-findlib/merge_requests/22 was
merged, so we may indeed pin to the main dev repos until a new findlib
is released.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions