aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/build
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-01 09:32:32 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-01 09:32:32 +0100
commit0048cbe810c82a775558c14cd7fcae644e205c51 (patch)
treee7d33757b34702d4d66a110a802bea307198d544 /dev/build
parent565c2c2a56e118d9cf9b6b72b623055bcd68af60 (diff)
parent559109c9b2c37b335f847c1460c1d75864e108e1 (diff)
Merge PR #736: [ci] Test coqchk on the CompCert target.
Diffstat (limited to 'dev/build')
0 files changed, 0 insertions, 0 deletions