Closed mtzguido closed 5 years ago
Hi guys, the build seems to be broken and I think we need this patch. I ran into this since I noticed an orange failure in F* CI. I haven't run a full build yet, leaving that to CI and will check back if it fails.
@R1kM will know; he may also have fixed it on mitls/dev already. Thanks Guido!
Oh, indeed it looks fixed in that branch.
Hi guys, the build seems to be broken and I think we need this patch. I ran into this since I noticed an orange failure in F* CI. I haven't run a full build yet, leaving that to CI and will check back if it fails.