From b207b8e6953d76af98e1d18983fb1467fc8fe8f5 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 16 Jun 2017 17:50:41 -0400
Subject: 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
```
---
 dev/ci/ci-common.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/ci/ci-common.sh')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 2711b7ecaa..d373ed3b19 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -59,7 +59,7 @@ install_ssreflect()
     sed -i.bak '/field/d'       Make && \
     sed -i.bak '/fingroup/d'    Make && \
     sed -i.bak '/algebra/d'     Make && \
-    make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install )
+    make Makefile.coq && make -f Makefile.coq all && make install )
 
   echo -en 'travis_fold:end:ssr.install\\r'
 
-- 
cgit v1.2.3