aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/nix
diff options
context:
space:
mode:
authorMaxime Dénès2020-09-28 09:15:49 +0200
committerMaxime Dénès2020-09-28 09:15:49 +0200
commit424ae427197126a2fcbd5f07eaa181fb6f81ad84 (patch)
treec29f6c916f25da23465b2932710f0b2a01002335 /dev/ci/nix
parent9c2228ff011dc6188b70084fa1e1a5158affcf24 (diff)
CI script wrapper now requires Python
Diffstat (limited to 'dev/ci/nix')
-rw-r--r--dev/ci/nix/default.nix3
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 741cb89eed..7863af842a 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -131,7 +131,8 @@ stdenv.mkDerivation {
name = "shell-for-${project}-in-${branch}";
buildInputs =
- optional withCoq coq
+ [ python ]
+ ++ optional withCoq coq
++ (prj.buildInputs or [])
++ optionals withCoq (prj.coqBuildInputs or [])
;