diff options
| author | Jason Gross | 2017-06-26 11:09:06 -0400 |
|---|---|---|
| committer | Jason Gross | 2017-07-21 03:36:47 -0400 |
| commit | 987655c3bc8a8ebd60856356f465b3c34eb4e252 (patch) | |
| tree | f41062a6a59d1fba4b655c564e54563cb7f3d1d7 /Makefile.ci | |
| parent | a0c84abf1f3078c1ba42df1b588acbac4bc2e4df (diff) | |
Separate make from python script for HoTT
HoTT still needs to use the submodule, but this will allow us to more easily see where the build fails, if it does
Diffstat (limited to 'Makefile.ci')
0 files changed, 0 insertions, 0 deletions