diff options
| author | Gaëtan Gilbert | 2018-04-16 19:29:56 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-04-16 19:29:56 +0200 |
| commit | a256e6f49d91fc79186c28607b86c7c3a5faf146 (patch) | |
| tree | c4f4c03c24f8c9aae6b11a23c7cc899912fac0ea /dev/ci | |
| parent | 3e7863e9369d38537685576a8642dbe0c062d0c5 (diff) | |
Travis: cleanup environment variables a bit.
- BUILD_TARGET not used
- Put elpi's FINDLIB_VER="" at the end of the environment for nicer
display in the travis UI.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions