aboutsummaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-03-06 16:33:47 +0100
committerMaxime Dénès2017-03-10 09:19:16 +0100
commitd30d5a9b32e020586d265f8e879c287269c17575 (patch)
treed0466aafd343aa0e944afec88c0ac047ecd32d87 /kernel/cemitcodes.ml
parenta99eea5165da3d91fe1d4b6560f9c53986c0c632 (diff)
[travis] Move GeoCoq to allow fail.
We need to agree a bit more with upstream.
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions