diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:54:15 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:54:15 +0100 |
| commit | 14c041012bd375cae018f83d107c836fca3d1f01 (patch) | |
| tree | 15e4d5608e4e60b6cbd6ece1bbe8c38100ddc3b5 /.github | |
| parent | 04d5253b91f7567a09b950caa420b69fc34c0d0e (diff) | |
| parent | 9879cc291512223c72a4cac2ef294c216cf64656 (diff) | |
Merge PR #6293: Check for Num lib if OCaml >= 4.06, fixes #6162
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions