diff options
| author | Théo Zimmermann | 2019-04-26 14:11:10 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-04-26 14:11:10 +0200 |
| commit | 025cb57a6f69c6a9c65e732656018d00d114be5c (patch) | |
| tree | 135e4ce0d4389a9f1441d72832ee00cf4deec200 /dev/base_include | |
| parent | e518ed1ff4121cd5e5be0e970c88e19bf29552c2 (diff) | |
| parent | 2d114afbf431f5cefe4f0350f95e22ef9daddfc9 (diff) | |
Merge PR #9990: [opam] Use version to provide better package bounds.
Reviewed-by: Zimmi48
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions