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/nativecode.ml | |
| parent | 21e9d207a8d8a0bee74c000f02a4e2819c53fae5 (diff) | |
| parent | 392c8f87bac1e47e18a2d7929bd01c2097b9e43a (diff) | |
Merge PR #9850: [dune] Don't have `lib` depend on `dynlink`
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions