diff options
| author | Maxime Dénès | 2017-07-11 14:44:14 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-11 14:44:14 +0200 |
| commit | 032e4f2bf5cb6eadba6ebbb16dd5d0c812dd2033 (patch) | |
| tree | 3a95561ee3e7fd3ae837cecf27b3692144d18d59 /dev/header | |
| parent | 8614fcd96d6fe538807099cde57f0c64d7e07b9d (diff) | |
| parent | 061dd5da6214485bfe79322db1973e773293b34b (diff) | |
Merge PR #858: [travis] Remove CompCert version check hack.
Diffstat (limited to 'dev/header')
0 files changed, 0 insertions, 0 deletions