diff options
| author | Jason Gross | 2019-01-16 17:02:12 -0500 |
|---|---|---|
| committer | Jason Gross | 2019-01-16 17:02:12 -0500 |
| commit | fc1756508a6cc5f756e08cdc7c108117025d4194 (patch) | |
| tree | ca2d55c777095effc6ded8b914d013abdb8eb1d4 /Makefile.doc | |
| parent | c5d4472e3df352188123a90ef53b7383d9e1ba55 (diff) | |
[ci] Update fiat-crypto to the new pipeline
We're recently reorganized fiat-crypto. This should fix the OOM CI
issues.
Fixes #9338
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions