aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorVincent Laporte2019-05-15 09:20:37 +0000
committerVincent Laporte2019-05-17 08:36:25 +0000
commit02d547e3bc531c9a0bec8d47436c204e3bc15ddc (patch)
tree8d26fe2543371b8353b4c56d6f8f6f2e80e067b7 /dev
parente9c2bc9aaddd401d18d90411ff68644b1d05c0d5 (diff)
[Nix-CI] Bignums no longer depends on camlp5
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/nix/bignums.nix2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix
index 1d931c858e..d813ddd8d7 100644
--- a/dev/ci/nix/bignums.nix
+++ b/dev/ci/nix/bignums.nix
@@ -1,5 +1,5 @@
{ ocamlPackages }:
{
- buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ];
+ buildInputs = [ ocamlPackages.ocaml ];
}