Skip to content

Comments

chore/prepare renaming#7

Merged
psteinroe merged 5 commits intomainfrom
chore/prepare-renaming
Oct 22, 2025
Merged

chore/prepare renaming#7
psteinroe merged 5 commits intomainfrom
chore/prepare-renaming

Conversation

@psteinroe
Copy link
Collaborator

we will now check if the new name is available, and fallback to the old one if not.

@psteinroe psteinroe merged commit bd6efdf into main Oct 22, 2025
1 check passed
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.

2 participants