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

Missing changelogs added between 8.16+rc1 and 8.16.0. #16386

Merged
merged 1 commit into from Aug 17, 2022
Merged

Missing changelogs added between 8.16+rc1 and 8.16.0. #16386

merged 1 commit into from Aug 17, 2022

Conversation

ppedrot
Copy link
Member

@ppedrot ppedrot commented Aug 17, 2022

No description provided.

@ppedrot ppedrot added the kind: documentation Additions or improvement to documentation. label Aug 17, 2022
@ppedrot ppedrot added this to the 8.16.0 milestone Aug 17, 2022
@ppedrot ppedrot requested a review from a team as a code owner August 17, 2022 13:46
@Alizter
Copy link
Contributor

Alizter commented Aug 17, 2022

By the way, I noticed a mistake in one of the changelogs:

Added: A deprecation warning that the :g:Class > syntax, that is currently doing nothing, will in the future declare

It should be "which is currently doing nothing"

@Zimmi48
Copy link
Member

Zimmi48 commented Aug 17, 2022

By the way, I noticed a mistake in one of the changelogs:

Added: A deprecation warning that the :g:Class > syntax, that is currently doing nothing, will in the future declare

It should be "which is currently doing nothing"

@Alizter if you open a PR fixing this, I can take care of merging it.

@Zimmi48 Zimmi48 self-assigned this Aug 17, 2022
Zimmi48
Zimmi48 approved these changes Aug 17, 2022
View reviewed changes
Copy link
Member

@Zimmi48 Zimmi48 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@coqbot merge now

@coqbot-app coqbot-app bot merged commit d6307ac into coq:master Aug 17, 2022
@coqbot-app coqbot-app bot added this to Request 8.16.0 inclusion in Coq 8.16 Aug 17, 2022
@jfehrle
Copy link
Member

jfehrle commented Aug 17, 2022

@Alizter Added: A deprecation warning that the :g:Class > syntax, that is currently doing nothing, will in the future declare

It should be "which is currently doing nothing"

Better "which currently does nothing". No need to use a progressive verb.

I can't find this changelog in master.

@ppedrot ppedrot deleted the changelog-8.16.0 branch August 17, 2022 16:46
ppedrot added a commit to ppedrot/coq that referenced this pull request Aug 17, 2022
@ppedrot
Backport PR coq#16386: Missing changelogs added between 8.16+rc1 and …
77e1f78 
…8.16.0.
@coqbot-app coqbot-app bot moved this from Request 8.16.0 inclusion to Shipped in 8.16.0 in Coq 8.16 Aug 17, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Zimmi48 Zimmi48 Zimmi48 approved these changes

Assignees

@Zimmi48 Zimmi48

Labels
kind: documentation Additions or improvement to documentation.
Projects
No open projects
Coq 8.16
  
Shipped in 8.16.0
Milestone
8.16.0
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@ppedrot @Alizter @Zimmi48 @jfehrle