diff options
| author | Emilio Jesus Gallego Arias | 2019-02-17 22:04:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-18 02:52:07 +0100 |
| commit | 3863a97b86a26e5f253db4e88a18f38a2cfc5ece (patch) | |
| tree | 9de24a948db5c76d08e5e8203a0b01093abf39e4 /dev/inc_ltac | |
| parent | a49077ef67b8e70696ecacc311fc3070d1b7b461 (diff) | |
[gitlab] [docker] [ci] Remove "edge" compiler switch.
Since a long time the compiler switch is not very useful as it is not
used to test any CI.
The `edge+flambda` version seems stable enough to carry out the `edge`
testing by itself, thus we remove the `egde` switch saving valuable
Docker image size and Gitlab runners.
We also tweak the `pkg:opam` job as to correctly set the version of
the pinned local package.
Diffstat (limited to 'dev/inc_ltac')
0 files changed, 0 insertions, 0 deletions