diff options
| author | Emilio Jesus Gallego Arias | 2020-09-17 17:32:16 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-09-17 17:32:16 +0200 |
| commit | 21366f8eab4ab9bd2c2af7a986b681704cd94c3f (patch) | |
| tree | 6df2be823134fcfa763885383a14afdff345fa55 /dev | |
| parent | 14f0e5059e7f49cabbcd1571d7f053db7d7d3f35 (diff) | |
[configure] Fix version checks for lablgtk and zarith
Fixes #13041 #13047
Configure is quite messy, but we will improve it once we can link it
with findlib and move to dune [that will actually allow to remove all
ad-hoc calls to `ocamlfind` in favor of `findlib` code.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions