Skip to content

Conversation

@LMG
Copy link
Collaborator

@LMG LMG commented Oct 24, 2025

No description provided.

@LMG
Copy link
Collaborator Author

LMG commented Oct 24, 2025

This fixes #1539

@LMG LMG force-pushed the remove_redirect branch 2 times, most recently from d13b70d to 783d22d Compare October 27, 2025 08:20
@christian-schilling christian-schilling added this pull request to the merge queue Oct 27, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to a conflict with the base branch Oct 27, 2025
@LMG LMG force-pushed the remove_redirect branch from 783d22d to 4461c6b Compare October 29, 2025 09:44
@LMG LMG force-pushed the remove_redirect branch from 4461c6b to e62d517 Compare October 29, 2025 11:34
@LMG LMG added this pull request to the merge queue Oct 29, 2025
Merged via the queue into master with commit bb045ee Oct 29, 2025
1 check passed
@LMG LMG deleted the remove_redirect branch October 29, 2025 14:36
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.

4 participants