diff options
| author | Maxime Dénès | 2017-07-19 01:14:21 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-19 01:14:21 +0200 |
| commit | 28b3bfd84718e5b29f8e3452fcfe22b19e9910dd (patch) | |
| tree | 999f38c098bb2fb5e2836273424411bf20e257bb /lib/pp.ml | |
| parent | 0315a5d93c2de996f5c91bd2af827d3984ec1ad8 (diff) | |
| parent | 80545721cc0bf019124996c2c45dc86d05625c77 (diff) | |
Merge PR #895: [ci] VST is now built with IGNORECOQVERSION=true.
Diffstat (limited to 'lib/pp.ml')
0 files changed, 0 insertions, 0 deletions