diff options
| author | Pierre-Marie Pédrot | 2020-05-13 12:55:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-13 13:01:28 +0200 |
| commit | 9e315837fded9763c3d7ca14a8aad0e7af3b4820 (patch) | |
| tree | de3f1189da6a868ae077c680fb14f2bca09d646c /dev | |
| parent | 3e04d6c024dd03878b0b487cf823f5586d6fd397 (diff) | |
Centralize the OCaml version-checking function.
We tweak the message a bit.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions