aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-fiat-crypto.sh
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-12-21 00:35:36 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-01-11 22:26:11 +0100
commit4a72f3bfe23edaa87307449b6033e7a296a93b04 (patch)
treeea6d8744f99fcc989c8bc744cea65a9b45e6eb05 /dev/ci/ci-fiat-crypto.sh
parent213b32325eb8d98133dc7a7f47f14d2d7af79a53 (diff)
Adding a custom Travis overlay for HoTT.
Diffstat (limited to 'dev/ci/ci-fiat-crypto.sh')
0 files changed, 0 insertions, 0 deletions