aboutsummaryrefslogtreecommitdiffhomepage
path: root/README.ci
Commit message (Collapse)AuthorAge
* Gitlab CIGravatar Gaëtan Gilbert2017-05-28
|
* [travis] Move ci files from `tools` to `dev`.Gravatar Maxime Dénès2017-02-07
|
* [travis] Improvements to main scriptGravatar Emilio Jesus Gallego Arias2017-02-07
- Add README.ci Suggestions and comments welcome. - Use the system compiler to get some boot speedup. - Build log folding. - Set NJOBS=2 (very moderate speedup) - Set language to a defined value. OPAM itself recommends C, so we follow suit. - Remove spurious `.opam`test No harm in testing we are in the right opam setting even if the cache did exist. Anyways, it seems that the previous was spurious, as it was testing if ~/coq/.opam did exists. I think the correct command would have been: ```shell [ -e ${HOME}/.opam ] || opam init ... ``` See the log at https://travis-ci.org/coq/coq/builds/198948812 for an example.