Skip to content

Conversation

@dumbbell
Copy link
Collaborator

@dumbbell dumbbell self-assigned this Jul 30, 2025
@mergify mergify bot added the make label Jul 30, 2025
@dumbbell dumbbell marked this pull request as ready for review July 30, 2025 10:50
@dumbbell dumbbell merged commit 4ac82b6 into main Jul 30, 2025
556 of 559 checks passed
@dumbbell dumbbell deleted the update-khepri-to-0.17.2 branch July 30, 2025 10:50
@michaelklishin
Copy link
Collaborator

@Mergifyio backport v4.1.x

@mergify mergify bot mentioned this pull request Jul 30, 2025
@michaelklishin michaelklishin added this to the 4.2.0 milestone Jul 30, 2025
@rabbitmq rabbitmq deleted a comment from mergify bot Jul 30, 2025
@dumbbell
Copy link
Collaborator Author

I don’t know how to clean the GitHub history. FTR, this pull request was never meant to be backported and was not effectively. The mention of a backport pull request above should be ignored. I can’t find a way to delete the pull request, or at least delete its mention here.

@michaelklishin
Copy link
Collaborator

The fact that the PR was closed is in and of itself an indicator that the idea was abandoned :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants