Skip to content

Update documentation from v2.2 release version to v2.3-dev #2557

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
Merged
merged 5 commits into from
Jan 18, 2025
Merged

Update documentation from v2.2 release version to v2.3-dev #2557

merged 5 commits into from
Jan 18, 2025

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Jan 16, 2025 •
edited
Loading

Fixes #2556 .

NB @MatthewDaggitt any other leftover admin tasks after the v2.2 release?
UPDATED: e.g.

  • CHANGELOG
  • doc/README.agda
  • copy v2.2 CHANGELOG to the CHANGELOG directory

@jamesmckinna jamesmckinna mentioned this pull request Jan 16, 2025
Merged
@jamesmckinna jamesmckinna mentioned this pull request Jan 16, 2025
Merged
@jamesmckinna jamesmckinna changed the title Update CHANGELOG from v2.2 release version to v2.3-dev Update documenttaion from v2.2 release version to v2.3-dev Jan 16, 2025
@jamesmckinna jamesmckinna changed the title Update documenttaion from v2.2 release version to v2.3-dev Update documentation from v2.2 release version to v2.3-dev Jan 16, 2025
@jamesmckinna jamesmckinna added this to the v2.3 milestone Jan 16, 2025
@MatthewDaggitt
Copy link
Contributor

Gah, I forgot about the reset. Sorry. The other thing that needs doing is:

  • Moving the changelog from the v2.2 tag to the CHANGELOG folder.

MatthewDaggitt
MatthewDaggitt approved these changes Jan 17, 2025
View reviewed changes
Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

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

After adding the v2.2. CHANGELOG this looks good to merge. Thanks!

@jamesmckinna
Copy link
Contributor Author

The other thing that needs doing is:

* Moving the changelog from the v2.2 tag to the `CHANGELOG` folder.

So... I did this by hand (as a copy, not a move?) because I'm not git-savvy enough to know how to do it magically from the v2.2 tag, but I hope the result is indistinguishable from what you intended... ;-)

@MatthewDaggitt MatthewDaggitt added this pull request to the merge queue Jan 18, 2025
Merged via the queue into agda:master with commit eded674 Jan 18, 2025
2 checks passed
@jamesmckinna jamesmckinna deleted the issue2556 branch February 3, 2025 09:05
@jamesmckinna jamesmckinna mentioned this pull request Jul 19, 2025
Merged
6 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@MatthewDaggitt MatthewDaggitt MatthewDaggitt approved these changes

Assignees
No one assigned
Labels
admin documentation
Projects
None yet
Milestone
v2.3
Development

Successfully merging this pull request may close these issues.

Clean up documentation to v2.3-dev after v2.2 release
2 participants
@jamesmckinna @MatthewDaggitt