Skip to content

Conversation

@eamodio
Copy link
Member

@eamodio eamodio commented Feb 10, 2025

Fixes #4035

@eamodio eamodio merged commit 93ed959 into main Feb 10, 2025
3 checks passed
@eamodio eamodio deleted the bug/#4035 branch February 19, 2025 20:03
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.

Repo is lost when "Generate commit" is requested

2 participants