Skip to content

fix: coe string -> name removed, explicitly call String.toName#67

Merged
Peiyang-Song merged 1 commit intolean-dojo:mainfrom
alok:fix-build-name
May 17, 2024
Merged

fix: coe string -> name removed, explicitly call String.toName#67
Peiyang-Song merged 1 commit intolean-dojo:mainfrom
alok:fix-build-name

Conversation

@alok
Copy link
Contributor

@alok alok commented Apr 28, 2024

The coercion was removed recently, and it's backwards compatible.

The coercion was removed recently, and it's backwards compatible.
@Peiyang-Song Peiyang-Song self-requested a review May 17, 2024 22:23
Copy link
Member

@Peiyang-Song Peiyang-Song left a comment

Choose a reason for hiding this comment

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

Merged, thanks!

@Peiyang-Song Peiyang-Song merged commit cf36e12 into lean-dojo:main May 17, 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.

2 participants