Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Simplify CircleCI script | 2018-04-15 | |
* | Remove from CircleCI builds that are already taken care of by Travis. | 2018-02-21 | |
* | ci: add elpi | 2018-02-19 | |
* | Merge PR #6601: Circle CI: fix cache selection. | 2018-01-31 | |
|\ | |||
* | | Fix CI with parallel make (messed up dependencies) | 2017-12-21 | |
| * | Circle CI: fix cache selection. | 2017-12-19 | |
|/ | |||
* | Circle CI: separate job to boot opam with all used packages. | 2017-12-14 | |
* | Circle CI: remove warning jobs | 2017-12-14 | |
* | Circle CI: uses dependencies between external developments. | 2017-12-13 | |
* | Circle CI: enable TIMED for external developments | 2017-12-13 | |
* | Circle CI: use cache for opam | 2017-12-13 | |
* | Circle CI: enable native compiler. | 2017-12-13 | |
* | Near-full implementation of Circle CI. | 2017-12-12 | |
* | CI: poc Circleci configuration | 2017-12-11 |