Skip to content

chore: rename Path.Id to PathType.Path#169

Merged
Jlh18 merged 1 commit intomasterfrom
PathType
Dec 11, 2025
Merged

chore: rename Path.Id to PathType.Path#169
Jlh18 merged 1 commit intomasterfrom
PathType

Conversation

@Jlh18
Copy link
Collaborator

@Jlh18 Jlh18 commented Dec 11, 2025

Renaming some things for consistency with upcoming Path type paper

@Jlh18 Jlh18 merged commit 0d3ac21 into master Dec 11, 2025
1 check passed
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.

1 participant