diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-16 17:50:41 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-16 17:51:59 -0400 |
| commit | b207b8e6953d76af98e1d18983fb1467fc8fe8f5 (patch) | |
| tree | 9a1059c2a8b9168bab0eaadc6112031da533d2bc /dev/ci/ci-cpdt.sh | |
| parent | 298264da86955277e1f392cc16bbbe6c416d995f (diff) | |
Remove -j ${NJOBS} from make invocations in the ci
According to
https://www.gnu.org/software/make/manual/html_node/Options_002fRecursion.html#Options_002fRecursion
it's not necessary, because we pass `-j ${NJOBS}` to the top-level `make`
invocation in `.travis.yml`. Additionally, explicitly passing `-j` in,
e.g., fiat-crypto, results in error messages such as
```
make[2]: *** write jobserver: Bad file descriptor. Stop.
make[2]: *** Waiting for unfinished jobs....
make[2]: *** write jobserver: Bad file descriptor. Stop.
make[1]: *** [coqprime] Error 2
make[1]: INTERNAL: Exiting with 1 jobserver tokens available; should be 2!
make[1]: Leaving directory `/home/travis/build/JasonGross/coq/_build_ci/fiat-c
```
because the `-j` on the `make` in the `ci-fiat-crypto.sh` script
disables jobserver mode, and the submake in fiat-crypto to make coqprime
does not explicitly pass `-j`, and so reenables jobserver mode, and then
`make` gets very confused.
Commit made with
```bash
cd dev/ci
git grep --name-only -- 'make -j ${NJOBS}' | xargs sed s'/make -j \${NJOBS}/make/g' -i
git grep --name-only -- 'make -f Makefile.coq -j ${NJOBS}' | xargs sed s'/make -f Makefile.coq -j \${NJOBS}/make -f Makefile.coq/g' -i
```
Diffstat (limited to 'dev/ci/ci-cpdt.sh')
| -rwxr-xr-x | dev/ci/ci-cpdt.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh index 0e791ebbf..8b725f6fe 100755 --- a/dev/ci/ci-cpdt.sh +++ b/dev/ci/ci-cpdt.sh @@ -6,5 +6,5 @@ source ${ci_dir}/ci-common.sh wget http://adam.chlipala.net/cpdt/cpdt.tgz tar xvfz cpdt.tgz -( cd cpdt && make clean && make -j ${NJOBS} ) +( cd cpdt && make clean && make ) |