diff options
| author | Pierre-Marie Pédrot | 2017-12-21 00:35:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-01-11 22:26:11 +0100 |
| commit | 4a72f3bfe23edaa87307449b6033e7a296a93b04 (patch) | |
| tree | ea6d8744f99fcc989c8bc744cea65a9b45e6eb05 /kernel | |
| parent | 213b32325eb8d98133dc7a7f47f14d2d7af79a53 (diff) | |
Adding a custom Travis overlay for HoTT.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions