Skip to content

Use final, idea by @clonker#61

Merged
msoos merged 2 commits intomasterfrom
use-final-by-moritz
Oct 4, 2025
Merged

Use final, idea by @clonker#61
msoos merged 2 commits intomasterfrom
use-final-by-moritz

Conversation

@msoos
Copy link
Copy Markdown
Collaborator

@msoos msoos commented Oct 2, 2025

Should be faster, and also actually semantically better. We never override this.

msoos added 2 commits October 2, 2025 20:18
Use final in override

Use override final

More final

More final

More final

More final
@msoos msoos force-pushed the use-final-by-moritz branch 2 times, most recently from 3bc423e to 5363d50 Compare October 3, 2025 10:26
@msoos msoos merged commit 1b6f7b9 into master Oct 4, 2025
36 checks passed
@msoos msoos deleted the use-final-by-moritz branch October 4, 2025 16:08
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