Closed fdupress closed 2 months ago
This appears to do the right thing: https://github.com/EasyCrypt/easycrypt/actions/runs/10722591238/job/29734178286?pr=608#step:6:1
(I was too slow to sneak the push to sha3 into the compilation time—I should have prepared it, or picked a shorter branch name...)
We need to check existence of a remote branch with refs/heads (otherwise, we would accept partial matches), but checkout without.
This should be checked by creating and pushing a branch
merge-fix-diversified-external-ci
in one of our external repositories, rather than just accepting the first set of CI results.