Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ci] Use docker-coq-action, mathcomp/mathcomp and mathcomp/mathcomp-dev #21

Merged
merged 6 commits into from
Jun 2, 2020

Conversation

erikmd
Copy link
Member

@erikmd erikmd commented Jun 2, 2020

Subsumes #16

@erikmd
Copy link
Member Author

erikmd commented Jun 2, 2020

I'm not sure to understand why, but it happens the last commit I pushed triggered a workflow in my fork only (for the push event), not in the math-comp/odd-order repo (for the pull_request event).

Even if the following thread is a bit old, it suggests this is related to a security mitigation:
https://github.community/t/run-a-github-action-on-pull-request-for-pr-opened-from-a-forked-repo/16054
but hopefully the CI status will directly work within the math-comp/odd-order PRs (including from forks) once the setup will be integrated in the default branch…

Anyway, let's wait for the on-going CI jobs to finish for the time being:
https://github.com/erikmd/odd-order/runs/730746813?check_suite_focus=true

@erikmd
Copy link
Member Author

erikmd commented Jun 2, 2020

done, the CI is green - in my fork

@erikmd
Copy link
Member Author

erikmd commented Jun 2, 2020

but maybe one should rename the opam file before merging this?

otherwise there is the:

Warning: the opam_file argument should have the '.opam' suffix.

@erikmd
Copy link
Member Author

erikmd commented Jun 2, 2020

hence the following CI run: https://github.com/erikmd/odd-order/actions/runs/122529017

@CohenCyril CohenCyril merged commit 30f44f9 into math-comp:master Jun 2, 2020
@erikmd erikmd deleted the use-docker-coq-action branch June 2, 2020 13:00
@CohenCyril CohenCyril mentioned this pull request Jun 2, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants