Skip to content

Rename Sub -> IsSub#44

Merged
msullivan merged 1 commit intomainfrom
sub-to-issub
Jan 17, 2026
Merged

Rename Sub -> IsSub#44
msullivan merged 1 commit intomainfrom
sub-to-issub

Conversation

@msullivan
Copy link
Collaborator

Yury says Guido would complain about Sub.

Yury says Guido would complain about `Sub`.
@msullivan msullivan requested a review from dnwpark January 17, 2026 00:40
@msullivan msullivan merged commit 202518e into main Jan 17, 2026
6 checks passed
@msullivan msullivan deleted the sub-to-issub branch January 17, 2026 00:41
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