aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-color.sh
Commit message (Expand)AuthorAge
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
| * Remove -j ${NJOBS} from make invocations in the ciGravatar Jason Gross2017-06-16
* | [travis] fix CoLoR by inserting some Require Import FunIndGravatar Pierre Letouzey2017-06-14
* | [travis] extra test ci-bignums (+factorize other scripts)Gravatar Pierre Letouzey2017-06-13
* | [travis] adapt CoLoR compilation to depend on the bignum packageGravatar Pierre Letouzey2017-06-13
| * [travis] [8.6.only] Backport latest changes from trunk.Gravatar Emilio Jesus Gallego Arias2017-03-22
* | [travis] Basic support for overlays.Gravatar Emilio Jesus Gallego Arias2017-03-13
* | [travis] Adding a template file and using it for all targets.Gravatar Théo Zimmermann2017-03-10
* | [travis] Change headband for wider compatibility.Gravatar Théo Zimmermann2017-03-10
| * [travis] Backport trunk's travis support.Gravatar Emilio Jesus Gallego Arias2017-03-02
* [travis] Move ci files from `tools` to `dev`.Gravatar Maxime Dénès2017-02-07