diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2017-06-11 20:22:43 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2017-06-11 20:22:43 -0400 |
| commit | 75f42c5c4f350f301ef1968459f4f19f7a349ad4 (patch) | |
| tree | 272ca2e26030fe1d4e487c68db3b0444ef4de29d /.gitignore | |
| parent | 79c42e22dd5106dcb85229ceec75331029ab5486 (diff) | |
Point ci-hott at a newer version of HoTT
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions