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

[CI] Exclude new ModelCategories from UniMath #18726

Merged
merged 1 commit into from Feb 28, 2024
Merged

[CI] Exclude new ModelCategories from UniMath #18726

merged 1 commit into from Feb 28, 2024

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Feb 28, 2024 •
edited

@proux01 proux01 added kind: infrastructure CI, build tools, development tools. part: CI The continuous integration system. request: full CI Use this label when you want your next push to trigger a full CI. labels Feb 28, 2024
@proux01 proux01 added this to the 8.20+rc1 milestone Feb 28, 2024
@proux01 proux01 requested a review from a team as a code owner February 28, 2024 14:15
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 28, 2024
@SkySkimmer SkySkimmer self-assigned this Feb 28, 2024
@proux01 proux01 mentioned this pull request Feb 28, 2024
Merged
5 tasks
@proux01
Copy link
Contributor Author

proux01 commented Feb 28, 2024

@SkySkimmer apparently unimath got through in 35min, so well below the 1h timeout, sounds good.

@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit cd966bb into coq:master Feb 28, 2024
5 of 6 checks passed
@proux01 proux01 deleted the ci_fix_unimath branch February 28, 2024 19:48
@proux01 proux01 mentioned this pull request Feb 29, 2024
Merged
6 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: infrastructure CI, build tools, development tools. part: CI The continuous integration system.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@proux01 @SkySkimmer