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

Consolidate credits and changelog information in a single place. #9668

Merged
merged 5 commits into from Apr 2, 2019

Conversation

@Zimmi48
Copy link
Member

commented Feb 28, 2019

This PR consolidates our credit chapter and our CHANGES file in a single place.

Following Enrico's proposal of using reverse chronological order for the recent credits, while keeping chronological order for older ones, the credits chapter is split in two parts:

The content of CHANGES (expect the unreleased version) and the historic (and archived) COMPATIBILITY file have been move into the new History and Changes chapters.

Later work includes:

  • Adopting a GitLab-like mode for the unreleased changes.
  • Implementing the proposal in #9103 by adding author and reviewer information to the changelog.
  • Moving the content of the CREDITS file to the History and Changes chapter as well.
  • Moving the ORCID info useful for Zenodo from the CREDITS file to the .mailmap file.

@Zimmi48 Zimmi48 added this to the 8.10+beta1 milestone Feb 28, 2019

@Zimmi48 Zimmi48 added this to History and changelog in Credits and license issues Feb 28, 2019

@Zimmi48 Zimmi48 changed the title Rm changes [wip] Consolidate credits and changelog information in a single place. Feb 28, 2019

Zimmi48 added some commits Feb 1, 2019

@Zimmi48 Zimmi48 force-pushed the Zimmi48:rm-CHANGES branch from 5b4ff9c to bdff9ab Mar 31, 2019

@Zimmi48 Zimmi48 changed the title [wip] Consolidate credits and changelog information in a single place. Consolidate credits and changelog information in a single place. Apr 1, 2019

@Zimmi48

This comment has been minimized.

Copy link
Member Author

commented Apr 1, 2019

@vbgl I propose to do this change in 8.10. For now, the CHANGES file is kept but contains only the unreleased changes. So an additional PR will be needed moving the content of this file to the Changes chapter after the release.

The plan is that the next version (8.11) will use a different mode for storing the change info, inspired by GitLab (and supported by @SkySkimmer). A branch showing what this would give is at https://github.com/Zimmi48/coq/tree/test-split-CHANGES/changelog.

@Zimmi48 Zimmi48 marked this pull request as ready for review Apr 1, 2019

@Zimmi48 Zimmi48 requested a review from coq/doc-maintainers as a code owner Apr 1, 2019

@cpitclaudel

This comment has been minimized.

Copy link
Contributor

commented Apr 2, 2019

LGTM. I'll wait for feedback from @vbgl to merge.

@vbgl

vbgl approved these changes Apr 2, 2019

Copy link
Contributor

left a comment

Thank you Théo!

@cpitclaudel cpitclaudel merged commit bdff9ab into coq:master Apr 2, 2019

7 of 9 checks passed

GitLab CI pipeline Pipeline completed with errors on GitLab CI
Details
plugin:ci-mtac2 script_failure on GitLab CI
Details
Pull request checks Passed.
Details
coq.coq Build #20190331.2 succeeded
Details
coq.coq (Windows) Windows succeeded
Details
coq.coq (macOS) macOS succeeded
Details
doc:ml-api:odoc: ml-api artifact Link to ml-api build artifact.
Details
doc:refman: refman artifact Link to refman build artifact.
Details
doc:refman: stdlib artifact Link to stdlib build artifact.
Details

cpitclaudel added a commit that referenced this pull request Apr 2, 2019

Merge PR #9668: Consolidate credits and changelog information in a si…
…ngle place.

Reviewed-by: cpitclaudel
Reviewed-by: vbgl

@Zimmi48 Zimmi48 deleted the Zimmi48:rm-CHANGES branch Apr 3, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.