aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-color.sh
Commit message (Expand)AuthorAge
* Improve shell scriptsGravatar zapashcanon2018-04-05
* Put bignums, math-classes and corn dependencies in MakefileGravatar Gaëtan Gilbert2017-12-13
* [ci] CoLoR has moved to githubGravatar Emilio Jesus Gallego Arias2017-12-07
* 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