Skip to content

[ add ] layout + boilerplate for deprecation warnings#2529

Merged
MatthewDaggitt merged 2 commits intoagda:masterfrom
jamesmckinna:pr2338-style-guide
Dec 27, 2024
Merged

[ add ] layout + boilerplate for deprecation warnings#2529
MatthewDaggitt merged 2 commits intoagda:masterfrom
jamesmckinna:pr2338-style-guide

Conversation

@jamesmckinna
Copy link
Collaborator

@MatthewDaggitt MatthewDaggitt added this to the v2.2 milestone Dec 24, 2024
@MatthewDaggitt MatthewDaggitt added this pull request to the merge queue Dec 27, 2024
Merged via the queue into agda:master with commit 4b790d4 Dec 27, 2024
@jamesmckinna jamesmckinna deleted the pr2338-style-guide branch December 27, 2024 07:06
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.

3 participants