diff options
| author | Emilio Jesus Gallego Arias | 2018-04-17 23:13:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-04-17 23:13:47 +0200 |
| commit | 8956ab2ff2c687f99c473bbd1849fbce36863fdc (patch) | |
| tree | 7dd3b5c18e630d962e35a6ae090a8460929e1b5e /dev/ci | |
| parent | c35c98c78295155db71ac80ea22adc7aef2d224e (diff) | |
| parent | 4847b99f691e4410d36e46d171a976228edb37b5 (diff) | |
Merge PR #7275: gitlab: separate opam-boot jobs, use opam init and OPAMROOT
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions