Matej Sima
|
c1910629e9
|
Remove Makefile, Add docker build command to the CI config
|
2019-05-24 00:13:31 +02:00 |
|
Christian Rinderknecht
|
cc706fc225
|
Gardening.
|
2019-05-16 15:28:28 +02:00 |
|
Georges Dupéron
|
8821e6c01e
|
Rewrite local opam repository into a different folder and .gitignore it
|
2019-05-15 16:45:37 +02:00 |
|
Georges Dupéron
|
834cc8c072
|
Missing stuff in gitlab-ci
|
2019-05-15 16:35:46 +02:00 |
|
Georges Dupéron
|
22b331dbed
|
Added tests to build, fixed some unused variables.
|
2019-05-15 15:17:04 +02:00 |
|
Georges Dupéron
|
5d17ddf4bb
|
gitlab-ci: opam init --bare to make the build faster
|
2019-05-14 19:52:48 +02:00 |
|
Georges Dupéron
|
b8f80b06f6
|
debug CI
|
2019-05-14 18:42:45 +02:00 |
|
Georges Dupéron
|
fadc84f76c
|
gitlab-ci.yml syntax
|
2019-05-14 18:17:39 +02:00 |
|
Georges Dupéron
|
586d772488
|
Renamed job, use git submodules in gitlab-ci
|
2019-05-14 18:16:14 +02:00 |
|
Georges Dupéron
|
60f99b3e9c
|
Moved script to rewrite OPAM repository outside of the .gitlab-ci.yml in ligo repo
|
2019-05-14 18:05:47 +02:00 |
|
Georges Dupéron
|
c43570a82d
|
Move into src/; add vendors/ subfolder, add CI script.
|
2019-05-14 17:53:44 +02:00 |
|