Skip to content
This repository was archived by the owner on Apr 1, 2025. It is now read-only.

Conversation

@SamB
Copy link
Contributor

@SamB SamB commented Aug 5, 2023

The old one stopped working :-(

@SamB SamB requested a review from a team as a code owner August 5, 2023 21:55
@SamB
Copy link
Contributor Author

SamB commented Aug 5, 2023

Sorry if this is the second time I opened a PR for this commit, but I accidentally deleted the branch and couldn't find the PR after that. (Perhaps I never actually submitted it?)

Copy link

@hendrikvanantwerpen hendrikvanantwerpen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for fixing the link!

@hendrikvanantwerpen
Copy link

@patrickt How do we get this merged? It's just a docs change, but CI is failing and it cannot be merged now.

@robrix robrix merged commit d7f9e09 into github:main Mar 25, 2024
@robrix
Copy link
Contributor

robrix commented Mar 25, 2024

Thanks very much for the fix, @SamB! Sorry it took so long to get merged, but very glad to have it.

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants