Skip to content

[ new ] un-deprecate _≈?_#3048

Open
gallais wants to merge 1 commit into
agda:masterfrom
gallais:char-eq-refactor
Open

[ new ] un-deprecate _≈?_#3048
gallais wants to merge 1 commit into
agda:masterfrom
gallais:char-eq-refactor

Conversation

@gallais

@gallais gallais commented Jul 2, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

As discussed in #3034

@jamesmckinna

jamesmckinna commented Jul 2, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Which master did you base this on? Surprised to still see the v1.5 deprecation still present... didn't #3034 kill that one off? UPDATED, I see It looks as though we left that one in place for precisely this PR...

jamesmckinna
jamesmckinna approved these changes Jul 2, 2026
View reviewed changes

@jamesmckinna jamesmckinna left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Happy with this, but a bit confused about how the CHANGELOG could/should record undeprecations? At the very least, there should be something under Additions to existing modules?

JacquesCarette
JacquesCarette approved these changes Jul 3, 2026
View reviewed changes

@JacquesCarette JacquesCarette left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Does this really need a CHANGELOG entry?

@jamesmckinna

jamesmckinna commented Jul 3, 2026

Copy link
Copy Markdown
Collaborator

Does this really need a CHANGELOG entry?

Well, not a hill on which I'd want to die, but... the question occurred to me. My own answer (it's an Addition...) at least seemed 'coherent'/'consistent' with existing practice. And there's the slight niggle at the back of my mind: otherwise, a change has been made, yet not recorded...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@JacquesCarette JacquesCarette JacquesCarette approved these changes
@jamesmckinna jamesmckinna jamesmckinna approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@gallais @jamesmckinna @JacquesCarette