Skip to content

fix CHANGELOG after #2418#2474

Merged
MatthewDaggitt merged 1 commit intoagda:masterfrom
jamesmckinna:fix-CHANGELOG
Sep 8, 2024
Merged

fix CHANGELOG after #2418#2474
MatthewDaggitt merged 1 commit intoagda:masterfrom
jamesmckinna:fix-CHANGELOG

Conversation

@jamesmckinna
Copy link
Collaborator

@jamesmckinna jamesmckinna commented Sep 5, 2024

See this comment et seq.

@MatthewDaggitt
Copy link
Collaborator

Thanks!

@MatthewDaggitt MatthewDaggitt added this to the v2.2 milestone Sep 8, 2024
@MatthewDaggitt MatthewDaggitt added this pull request to the merge queue Sep 8, 2024
Merged via the queue into agda:master with commit 4e87466 Sep 8, 2024
@jamesmckinna jamesmckinna deleted the fix-CHANGELOG branch December 21, 2024 09:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants