diff options
| author | Arnaud Spiwack | 2017-12-08 20:00:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-12-11 21:09:42 +0100 |
| commit | e5922809138d45fb29677577c7f8822875b5b67b (patch) | |
| tree | ad1f6dd1db615df48fd482a9efb156b8eb6d0102 /dev/header | |
| parent | a77f3a3e076e273af35ad520cae2eef0e3552811 (diff) | |
CI: poc Circleci configuration
Revert "CI: poc Circleci configuration"
Committed on master by mistake. Clearly I'm too clumsy to be trusted
with push rights.
This reverts commit d606a85d53fbd0227b15e18701e2ac4c9d911f34.
CI: poc Circleci configuration
Fixup
Try minimising build for faster testing
Various fixes
Fixup: yaml identation
Do not -j2: native compiler seems to take too much memory
Revert "Do not -j2: native compiler seems to take too much memory"
This reverts commit 4886151288a8d895c0fd23f9bded0970c59e1372.
Deactivate native compiler
Fixup (how did this happen?)
Do not call time (not install on docker images, will fix later)
Fixup
Fixup
Diffstat (limited to 'dev/header')
0 files changed, 0 insertions, 0 deletions