aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-compcert.sh
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-16 17:50:41 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-16 17:51:59 -0400
commitb207b8e6953d76af98e1d18983fb1467fc8fe8f5 (patch)
tree9a1059c2a8b9168bab0eaadc6112031da533d2bc /dev/ci/ci-compcert.sh
parent298264da86955277e1f392cc16bbbe6c416d995f (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-compcert.sh')
-rwxr-xr-xdev/ci/ci-compcert.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index c78ffdc2c..0dd904648 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -9,4 +9,4 @@ opam install -j ${NJOBS} -y menhir
git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
# Patch to avoid the upper version limit
-( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
+( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make )