aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorThéo Zimmermann2019-03-19 17:55:58 +0100
committerThéo Zimmermann2019-03-19 17:55:58 +0100
commit0a2773c90b69e301ec1d7203e8188694244b0167 (patch)
tree747fb9d6280cf313a087435319ed9201aeb556ce /dev
parent2b68b2223527b5bc247bd338ae4613a00654636c (diff)
parent3219cf3d4f308153a6ed0d48faee0eb056ccf0de (diff)
Merge PR #9647: [default.nix] Enable parallel build
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/nix/coq.nix1
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/ci/nix/coq.nix b/dev/ci/nix/coq.nix
index ecd280e58d..b610790f61 100644
--- a/dev/ci/nix/coq.nix
+++ b/dev/ci/nix/coq.nix
@@ -5,5 +5,4 @@ let coq = callPackage wd { buildDoc = false; doInstallCheck = false; coq-version
coq.overrideAttrs (o: {
name = "coq-local-${branch}";
src = fetchGit "${wd}";
- enableParallelBuilding = true;
})