diff options
| author | Gaëtan Gilbert | 2017-12-11 15:43:34 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-12-12 15:24:45 +0100 |
| commit | 8323ac57d63d3734c5f43b787c97644bf2fce32d (patch) | |
| tree | 83279e6bc1432e64bd4e226e9382ae73e98924de /dev/base_include | |
| parent | e5922809138d45fb29677577c7f8822875b5b67b (diff) | |
Near-full implementation of Circle CI.
VS gitlab:
+ fiat-crypto (Circle has 4GB RAM, gitlab 2GB)
- caching opam (TODO)
- publishing artefacts (TODO)
* tests with -local, not installed
VS travis:
+ reusing build products
- flambda validate job (TODO?)
- OSX jobs (TODO at least check if free OSX is possible)
- linter (TODO?)
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions