-
Notifications
You must be signed in to change notification settings - Fork 14
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
Support for @coqbot run full CI
in PR body.
#286
Comments
A related idea came up when discussing with @jnarboux during GDR GPL 2024 days "GT logiciel ecoresponsable" session: We could include a checklist to decide what kind of CI to run in the PR template (e.g., doc only PRs could have a build doc checkbox, etc.). coqbot could pick on this and use it to only run what is necessary for default pipelines. Being in the PR template, it would be more discoverable. This feature requires some implementation in the GitLab CI configuration that is also needed for a similar feature that is long awaited and would allow launching a single job rather than a full pipeline when we need to test compatibility with a specific project. |
Currently, it is only taken into account in PR comments or review comments.
Examples show that users forget about the
request: full CI
label and want to use the command in the PR body instead: coq/coq#17684The text was updated successfully, but these errors were encountered: