diff options
| author | Gaëtan Gilbert | 2019-03-23 23:51:26 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-23 23:51:26 +0100 |
| commit | e8fd832d9e487fa57e2efe627223d04ff2977fa9 (patch) | |
| tree | ac85641a010fd7011f49a629df4fcd2b6553828c /.github | |
| parent | 1d68c24736b4cf68ac0c2f70122e3f3d28f0e876 (diff) | |
| parent | ffc088b15b75f0d0577811df48b3511ab9942d1c (diff) | |
Merge PR #9822: [ci] [gitlab] Pin ocamlfind to master
Reviewed-by: SkySkimmer
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions