diff options
| author | Maxime Dénès | 2017-04-24 13:32:14 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-24 13:32:14 +0200 |
| commit | 3ba5dc3be9767422a6874fef034041a36b34f620 (patch) | |
| tree | 7d2b9a0e16e6e027dba8c4cc63dcae11789504d5 /plugins | |
| parent | d1a7206c3c9d89f1be8446be75bf0e5d90128087 (diff) | |
| parent | 6d2712cc7403ab05afb0f95b1a7d44c6e2acc518 (diff) | |
Merge PR#492: [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions