Skip to content

Use final, idea by @clonker#791

Merged
msoos merged 1 commit intomasterfrom
final-by-moritz
Oct 2, 2025
Merged

Use final, idea by @clonker#791
msoos merged 1 commit intomasterfrom
final-by-moritz

Conversation

@msoos
Copy link
Copy Markdown
Owner

@msoos msoos commented Oct 2, 2025

Should be faster and also semantically more sane. We never override this further.

@msoos msoos closed this Oct 2, 2025
@msoos msoos deleted the final-by-moritz branch October 2, 2025 19:38
@msoos msoos restored the final-by-moritz branch October 2, 2025 19:38
@msoos msoos reopened this Oct 2, 2025
@msoos msoos merged commit b7c039f into master Oct 2, 2025
38 checks passed
@msoos msoos deleted the final-by-moritz branch April 2, 2026 20:40
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