diff options
| author | Gaëtan Gilbert | 2020-04-10 10:14:48 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-10 10:14:48 +0200 |
| commit | e34cae33d494f4ad1a4a27c94a323a160dc67d9f (patch) | |
| tree | 8f01c3c58dea3e2ea13764aaac215c83f51fcf8b /plugins | |
| parent | 795df4b7a194b53b592ed327d2318ef5abc7d131 (diff) | |
| parent | c7b82d512e15c857cf8176dfae9584fdf203fafa (diff) | |
Merge PR #12036: [ci] [fiat-crypto] [flambda] Don't use flambda for fiat-crypto
Reviewed-by: SkySkimmer
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions