aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/subtyping.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-05 19:23:49 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-07 20:23:17 +0200
commitcde263581c49a75f8abdbcb398511942906e6204 (patch)
tree615d8c5f4e824aeaeec7a8ce317638fe41cd8355 /checker/subtyping.ml
parent612ca9e742c3196ea5faad100bb95d9e08ebe07e (diff)
[gitlab] Add bleeding-edge flambda build.
We also introduce a bit more systematic job naming: `base/edge`. In order to make the flambda switch selectable we update the Docker image so all the dependencies are installed in that one. Note the extra quote rule for the flambda parameters, but unless we can assign arrays to Gitlab variables there is not a good way to do this I'm afraid. With this patch we are getting close to being able to remove most builds from Travis.
Diffstat (limited to 'checker/subtyping.ml')
0 files changed, 0 insertions, 0 deletions