diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-07-18 15:56:54 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-07-18 15:56:54 +0200 |
commit | 80545721cc0bf019124996c2c45dc86d05625c77 (patch) | |
tree | 999f38c098bb2fb5e2836273424411bf20e257bb /dev/ci/ci-metacoq.sh | |
parent | 0315a5d93c2de996f5c91bd2af827d3984ec1ad8 (diff) |
[ci] VST is now built with IGNORECOQVERSION=true.
Diffstat (limited to 'dev/ci/ci-metacoq.sh')
0 files changed, 0 insertions, 0 deletions