Skip to content

Conversation

@reneSchm
Copy link
Member

This PR works around an apparent github bug in #1475. Look at #1475 for the review of this code.

reneSchm and others added 5 commits January 12, 2026 18:00
@reneSchm reneSchm changed the base branch from dummy to main January 14, 2026 14:23
@reneSchm reneSchm requested a review from HenrZu January 14, 2026 14:23
Copy link
Contributor

@HenrZu HenrZu left a comment

Choose a reason for hiding this comment

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

Already approved in bugged PR (see description in this PR)

@reneSchm reneSchm merged commit 54aa7db into main Jan 14, 2026
@reneSchm reneSchm deleted the improve-compile-time-of-index_of_type branch January 14, 2026 14:25
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