Skip to content

name_of is obsolete, replaced by identifier_of#33

Merged
FranciscoThiesen merged 1 commit intomainfrom
reformatting
Jul 18, 2024
Merged

name_of is obsolete, replaced by identifier_of#33
FranciscoThiesen merged 1 commit intomainfrom
reformatting

Conversation

@lemire
Copy link
Copy Markdown
Member

@lemire lemire commented Jul 18, 2024

No description provided.

@lemire lemire requested a review from FranciscoThiesen July 18, 2024 00:08
@CarlosEduR
Copy link
Copy Markdown
Member

It looks good to me

@FranciscoThiesen
Copy link
Copy Markdown
Member

Thanks for quickly fixing this!

@FranciscoThiesen FranciscoThiesen merged commit 2680090 into main Jul 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants