aboutsummaryrefslogtreecommitdiff
path: root/.circleci
AgeCommit message (Expand)Author
2018-02-21Remove from CircleCI builds that are already taken care of by Travis.Théo Zimmermann
2018-02-19ci: add elpiEnrico Tassi
2018-01-31Merge PR #6601: Circle CI: fix cache selection.Maxime Dénès
2017-12-21Fix CI with parallel make (messed up dependencies)Gaëtan Gilbert
2017-12-19Circle CI: fix cache selection.Gaëtan Gilbert
2017-12-14Circle CI: separate job to boot opam with all used packages.Gaëtan Gilbert
2017-12-14Circle CI: remove warning jobsGaëtan Gilbert
2017-12-13Circle CI: uses dependencies between external developments.Gaëtan Gilbert
2017-12-13Circle CI: enable TIMED for external developmentsGaëtan Gilbert
2017-12-13Circle CI: use cache for opamGaëtan Gilbert
2017-12-13Circle CI: enable native compiler.Gaëtan Gilbert
2017-12-12Near-full implementation of Circle CI.Gaëtan Gilbert
2017-12-11CI: poc Circleci configurationArnaud Spiwack