diff options
| author | Gaëtan Gilbert | 2018-03-30 17:06:18 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-03-30 17:06:18 +0200 |
| commit | 7cec7d312831f509a2d63e89173395ee428f46fa (patch) | |
| tree | b960d14e718ae03885442082de5590e12ae54ffc /dev | |
| parent | c0eedb5bdcb815132f404e19d6bf59730ae6e2df (diff) | |
gitlab: fix environment for build template
When `build` was made to build the doc it dropped `-coqide opt` and
dropped the environment variables for building coqide.
The combination means that when the cache had lablgtk in
opam (installed by some other job) configure would pick it up but the
system package wouldn't be there causing a failure. When lablgtk isn't
in the cache everything was fine.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions