diff options
| author | Emilio Jesus Gallego Arias | 2017-02-06 21:34:39 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-02-07 02:15:07 +0100 |
| commit | 486ad00de3ec88adea5e770c29142210e9de8b97 (patch) | |
| tree | 6ece32501417f8a7081b6464783094886fe2aa76 | |
| parent | ab3eda33281366194e1eadb5c53970da8fd3b3b5 (diff) | |
[travis] Improve parallelism in build (cf #88)
| -rw-r--r-- | .travis.yml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/.travis.yml b/.travis.yml index 966c910..b7f69d9 100644 --- a/.travis.yml +++ b/.travis.yml @@ -48,5 +48,6 @@ script: - cd mathcomp # Full build takes too much time. - sed -i.bak '/odd_order/d' Make -- make -j ${NJOBS} +- make Makefile.coq +- make -f Makefile.coq -j ${NJOBS} all - echo -en 'travis_fold:end:mathcomp.build\\r' |