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

Changelog for #18224 #18798

Merged
merged 1 commit into from Mar 19, 2024
Merged

Changelog for #18224 #18798

merged 1 commit into from Mar 19, 2024

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Mar 14, 2024

Changelog for #18224

@proux01 proux01 added the kind: documentation Additions or improvement to documentation. label Mar 14, 2024
@proux01 proux01 added this to the 8.20+rc1 milestone Mar 14, 2024
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 14, 2024
@proux01 proux01 removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 14, 2024
@SkySkimmer SkySkimmer self-assigned this Mar 18, 2024
@SkySkimmer SkySkimmer added the needs: progress Work in progress: awaiting action from the author. label Mar 18, 2024
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 18, 2024
@proux01 proux01 removed needs: progress Work in progress: awaiting action from the author. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Mar 18, 2024
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit f477f45 into coq:master Mar 19, 2024
6 checks passed
@proux01 proux01 deleted the changelog_18224 branch March 19, 2024 13:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: documentation Additions or improvement to documentation.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants