aboutsummaryrefslogtreecommitdiff
path: root/kernel/dune
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-03-14 05:14:07 +0100
committerEmilio Jesus Gallego Arias2019-03-28 00:56:23 +0100
commit392c8f87bac1e47e18a2d7929bd01c2097b9e43a (patch)
tree9cb5ce75d8cac6f10d5c0a9c73de4b2d14975666 /kernel/dune
parenta796822e5f57f74ff36e538fd2169f70a8c6c145 (diff)
[dune] Don't have `lib` depend on `dynlink`
This is convenient for the bootstrap of `coqdep`
Diffstat (limited to 'kernel/dune')
-rw-r--r--kernel/dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/dune b/kernel/dune
index a8a87a3e95..5b23a705ae 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -4,7 +4,7 @@
(public_name coq.kernel)
(wrapped false)
(modules (:standard \ genOpcodeFiles uint63_x86 uint63_amd64 write_uint63))
- (libraries lib byterun))
+ (libraries lib byterun dynlink))
(executable
(name genOpcodeFiles)