diff options
| author | Théo Zimmermann | 2019-03-28 08:54:25 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-28 08:54:25 +0100 |
| commit | 383bcf46b12799762fefec7e06fe00b5e33f5a18 (patch) | |
| tree | 02f610e7c5de11820ce0409dfb6c574b91012bbc /kernel | |
| parent | 21e9d207a8d8a0bee74c000f02a4e2819c53fae5 (diff) | |
| parent | 392c8f87bac1e47e18a2d7929bd01c2097b9e43a (diff) | |
Merge PR #9850: [dune] Don't have `lib` depend on `dynlink`
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/dune | 2 |
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) |