diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-04-24 13:32:14 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-24 13:32:14 +0200 |
commit | 3ba5dc3be9767422a6874fef034041a36b34f620 (patch) | |
tree | 7d2b9a0e16e6e027dba8c4cc63dcae11789504d5 /test-suite/bugs/opened/2652a.v-disabled | |
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 'test-suite/bugs/opened/2652a.v-disabled')
0 files changed, 0 insertions, 0 deletions