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.

Sign up for GitHub

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

Jump to bottom

Support for @coqbot run full CI in PR body. #286

Open
Zimmi48 opened this issue Jun 5, 2023 · 1 comment
Open

Support for @coqbot run full CI in PR body. #286

Zimmi48 opened this issue Jun 5, 2023 · 1 comment
Labels
enhancement New feature or request

Comments

@Zimmi48
Copy link
Member

Zimmi48 commented Jun 5, 2023

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#17684
@ticket-tagger ticket-tagger bot added the enhancement New feature or request label Jun 5, 2023
@Zimmi48
Copy link
Member Author

Zimmi48 commented Jun 5, 2024

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@Zimmi48